Adapt to coq/coq#14928

rocq-archive · Oct 9, 2023 · 6683f09 · 6683f09
1 parent 7d9e619
commit 6683f09
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 0 deletions.
diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml
@@ -139,6 +139,9 @@ type explicit_flag = [%import: Constrexpr.explicit_flag]
 (* type sign = [%import: Constrexpr.sign]
  *   [@@deriving sexp,yojson] *)
 
+type delimiter_depth = [%import: Constrexpr.delimiter_depth]
+  [@@deriving sexp,yojson,hash,compare]
+
 type prim_token = [%import: Constrexpr.prim_token]
   [@@deriving sexp,yojson,hash,compare]
 

diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli
@@ -62,6 +62,9 @@ val sexp_of_binder_kind : binder_kind -> Sexp.t
  * val proj_flag_of_sexp : Sexp.t -> proj_flag
  * val sexp_of_proj_flag : proj_flag -> Sexp.t *)
 
+type delimiter_depth = [%import: Constrexpr.delimiter_depth]
+  [@@deriving sexp,yojson,hash,compare]
+
 type prim_token = Constrexpr.prim_token
 
 val prim_token_of_sexp : Sexp.t -> prim_token

diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml
@@ -59,6 +59,9 @@ type goal_identifier = [%import: Vernacexpr.goal_identifier]
 type scope_name      = [%import: Vernacexpr.scope_name]
   [@@deriving sexp,yojson,hash,compare]
 
+type scope_delimiter = [%import: Vernacexpr.scope_delimiter]
+  [@@deriving sexp,yojson,hash,compare]
+
 type goal_reference =
   [%import: Vernacexpr.goal_reference]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli
@@ -23,6 +23,10 @@ type scope_name =
   [%import: Vernacexpr.scope_name]
   [@@deriving sexp,yojson]
 
+type scope_delimiter =
+  [%import: Vernacexpr.scope_delimiter]
+  [@@deriving sexp,yojson]
+
 type notation_format =
   [%import: Vernacexpr.notation_format]
   [@@deriving sexp,yojson]