Merge pull request #304 from herbelin/master+fix12467-inconsistency-b…

…inderlist-termlist-notation
rocq-archive · Feb 14, 2023 · bde3fcd · bde3fcd
2 parents 02d287c + f165160
commit bde3fcd
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/serlib/ser_extend.ml b/serlib/ser_extend.ml
@@ -38,6 +38,10 @@ type binder_entry_kind =
   [%import: Extend.binder_entry_kind]
   [@@deriving sexp]
 
+and constr_prod_entry_key =
+  [%import: Extend.constr_prod_entry_key]
+  [@@deriving sexp]
+
 type 'lev constr_entry_key_gen =
   [%import: 'lev Extend.constr_entry_key_gen]
   [@@deriving sexp,yojson,hash,compare]
@@ -46,10 +50,6 @@ type constr_entry_key =
   [%import: Extend.constr_entry_key]
   [@@deriving sexp,yojson,hash,compare]
 
-type constr_prod_entry_key =
-  [%import: Extend.constr_prod_entry_key]
-  [@@deriving sexp]
-
 type simple_constr_prod_entry_key =
   [%import: Extend.simple_constr_prod_entry_key]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_notation_term.ml b/serlib/ser_notation_term.ml
@@ -43,8 +43,8 @@ type subscopes =
 (*   [%import: Notation_term.syntax_modifier] *)
 (*   [@@deriving sexp] *)
 
-type constr_as_binder_kind =
-  [%import: Notation_term.constr_as_binder_kind]
+type notation_binder_kind =
+  [%import: Notation_term.notation_binder_kind]
   [@@deriving sexp,yojson,hash,compare]
 
 type notation_var_internalization_type =

diff --git a/serlib/ser_notation_term.mli b/serlib/ser_notation_term.mli
@@ -16,7 +16,7 @@
 type subscopes = Notation_term.subscopes
   [@@deriving sexp,yojson,hash,compare]
 
-type constr_as_binder_kind = Notation_term.constr_as_binder_kind
+type notation_binder_kind = Notation_term.notation_binder_kind
   [@@deriving sexp,yojson,hash,compare]
 
 type notation_var_internalization_type = Notation_term.notation_var_internalization_type