Adapt to Coq PR #19301

- proof_expr is generalized into body_expr - definition_expr subsumes fixpoint_expr_gen
ejgallego · Oct 23, 2024 · 746a134 · 746a134
1 parent 9235b2f
commit 746a134
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 16 deletions.
diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml
@@ -132,6 +132,10 @@ type option_setting =
  *   [%import: Vernacexpr.sort_expr]
  *   [@@deriving sexp,yojson,hash,compare] *)
 
+type body_expr =
+  [%import: Vernacexpr.body_expr]
+  [@@deriving sexp,yojson,hash,compare]
+
 type definition_expr =
   [%import: Vernacexpr.definition_expr]
   [@@deriving sexp,yojson,hash,compare]
@@ -160,10 +164,6 @@ type recursion_order_expr =
   [%import: Vernacexpr.recursion_order_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type recursive_expr_gen =
-  [%import: Vernacexpr.recursive_expr_gen]
-  [@@deriving sexp,yojson,hash,compare]
-
 type fixpoint_expr =
   [%import: Vernacexpr.fixpoint_expr]
   [@@deriving sexp,yojson,hash,compare]
@@ -245,10 +245,6 @@ type one_inductive_expr =
   [%import: Vernacexpr.one_inductive_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type proof_expr =
-  [%import: Vernacexpr.proof_expr]
-  [@@deriving sexp,yojson,hash,compare]
-
 type opacity_flag =
   [%import: Vernacexpr.opacity_flag]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli
@@ -104,6 +104,10 @@ type locality_flag =
   [%import: Vernacexpr.locality_flag]
   [@@deriving sexp,yojson,hash,compare]
 
+type body_expr =
+  [%import: Vernacexpr.body_expr]
+  [@@deriving sexp,yojson,hash,compare]
+
 type definition_expr =
   [%import: Vernacexpr.definition_expr]
   [@@deriving sexp,yojson,hash,compare]
@@ -116,10 +120,6 @@ type recursion_order_expr =
   [%import: Vernacexpr.recursion_order_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type recursive_expr_gen =
-  [%import: Vernacexpr.recursive_expr_gen]
-  [@@deriving sexp,yojson,hash,compare]
-
 type fixpoint_expr =
   [%import: Vernacexpr.fixpoint_expr]
   [@@deriving sexp,yojson,hash,compare]
@@ -184,10 +184,6 @@ type one_inductive_expr =
   [%import: Vernacexpr.one_inductive_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type proof_expr =
-  [%import: Vernacexpr.proof_expr]
-  [@@deriving sexp,yojson,hash,compare]
-
 type proof_end =
   [%import: Vernacexpr.proof_end]
   [@@deriving sexp,yojson,hash,compare]