Adapt to Coq PR #19404

ejgallego · Jul 21, 2024 · cef5176 · cef5176
1 parent 9235b2f
commit cef5176
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 6 deletions.
diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml
@@ -165,10 +165,15 @@ type delimiter_depth = [%import: Constrexpr.delimiter_depth]
 type prim_token = [%import: Constrexpr.prim_token]
   [@@deriving sexp,yojson,hash,compare]
 
+type ('a,'b,'c) notation_arg_kind = [%import: ('a,'b,'c) Constrexpr.notation_arg_kind]
+  [@@deriving sexp,yojson,hash,compare]
+
+type ('a,'b,'c) notation_arg_type = [%import: ('a,'b,'c) Constrexpr.notation_arg_type]
+  [@@deriving sexp,yojson,hash,compare]
+
 type cases_pattern_expr_r = [%import: Constrexpr.cases_pattern_expr_r]
 and cases_pattern_expr = [%import: Constrexpr.cases_pattern_expr]
 and kinded_cases_pattern_expr = [%import: Constrexpr.kinded_cases_pattern_expr]
-and cases_pattern_notation_substitution = [%import: Constrexpr.cases_pattern_notation_substitution]
 and constr_expr_r = [%import: Constrexpr.constr_expr_r]
 and constr_expr = [%import: Constrexpr.constr_expr]
 and case_expr   = [%import: Constrexpr.case_expr]
@@ -178,7 +183,8 @@ and cofix_expr  = [%import: Constrexpr.cofix_expr]
 and fixpoint_order_expr_r = [%import: Constrexpr.fixpoint_order_expr_r]
 and fixpoint_order_expr = [%import: Constrexpr.fixpoint_order_expr]
 and local_binder_expr    = [%import: Constrexpr.local_binder_expr]
-and constr_notation_substitution = [%import: Constrexpr.constr_notation_substitution]
+and notation_arg_type_expr = [%import: Constrexpr.notation_arg_type_expr]
+and notation_substitution = [%import: Constrexpr.notation_substitution]
   [@@deriving sexp,yojson,hash,compare]
 
 type constr_pattern_expr = [%import: Constrexpr.constr_pattern_expr]

diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli
@@ -74,13 +74,10 @@ val prim_token_of_sexp : Sexp.t -> prim_token
 val sexp_of_prim_token : prim_token -> Sexp.t
 
 type cases_pattern_expr = Constrexpr.cases_pattern_expr
-and cases_pattern_notation_substitution = Constrexpr.cases_pattern_notation_substitution
 
 val cases_pattern_expr_of_sexp : Sexp.t -> cases_pattern_expr
-val cases_pattern_notation_substitution_of_sexp : Sexp.t -> cases_pattern_notation_substitution
 
 val sexp_of_cases_pattern_expr : cases_pattern_expr -> Sexp.t
-val sexp_of_cases_pattern_notation_substitution : cases_pattern_notation_substitution -> Sexp.t
 
 type instance_expr = Constrexpr.instance_expr
 
@@ -94,7 +91,7 @@ and fix_expr             = Constrexpr.fix_expr
 and cofix_expr           = Constrexpr.cofix_expr
 and fixpoint_order_expr = Constrexpr.fixpoint_order_expr
 and local_binder_expr    = Constrexpr.local_binder_expr
-and constr_notation_substitution = Constrexpr.constr_notation_substitution
+and notation_substitution = Constrexpr.notation_substitution
 [@@deriving sexp, yojson, hash,compare]
 
 type constr_pattern_expr = Constrexpr.constr_pattern_expr [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_genintern.ml b/serlib/ser_genintern.ml
@@ -36,6 +36,10 @@ module Store = struct
 
 end
 
+type notation_variable_status =
+  [%import: Genintern.notation_variable_status]
+  [@@deriving sexp, yojson, hash, compare]
+
 type intern_variable_status =
   [%import: Genintern.intern_variable_status]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_genintern.mli b/serlib/ser_genintern.mli
@@ -20,6 +20,9 @@ open Sexplib
 
 module Store : SerType.SJHC with type t = Genintern.Store.t
 
+type notation_variable_status = Genintern.notation_variable_status
+  [@@deriving sexp, yojson, hash, compare]
+
 type intern_variable_status = Genintern.intern_variable_status
   [@@deriving sexp, yojson, hash, compare]