Adapt to Coq PR #19301, continued

- ident_decl -> decl_ident - notation_declaration -> decl_notation
ejgallego · Oct 27, 2024 · 9da9f97 · 9da9f97
1 parent 746a134
commit 9da9f97
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli
@@ -31,8 +31,8 @@ type entry_relative_level = Constrexpr.entry_relative_level [@@deriving sexp, yo
 type notation_entry_relative_level = Constrexpr.notation_entry_relative_level [@@deriving sexp, yojson, hash,compare]
 
 type universe_decl_expr = Constrexpr.universe_decl_expr [@@deriving sexp, yojson, hash,compare]
-type ident_decl = Constrexpr.ident_decl [@@deriving sexp, yojson, hash,compare]
-type cumul_ident_decl = Constrexpr.cumul_ident_decl [@@deriving sexp, yojson, hash,compare]
+type decl_ident = Constrexpr.decl_ident [@@deriving sexp, yojson, hash,compare]
+type decl_ident_cumul = Constrexpr.decl_ident_cumul [@@deriving sexp, yojson, hash,compare]
 type univ_constraint_expr = Constrexpr.univ_constraint_expr [@@deriving sexp, yojson, hash,compare]
 type name_decl = Constrexpr.name_decl [@@deriving sexp, yojson, hash,compare]
 

diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli
@@ -112,8 +112,8 @@ type definition_expr =
   [%import: Vernacexpr.definition_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type notation_declaration =
-  [%import: Vernacexpr.notation_declaration]
+type decl_notation =
+  [%import: Vernacexpr.decl_notation]
   [@@deriving sexp,yojson,hash,compare]
 
 type recursion_order_expr =