diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli
index 977258fa..2d41ec70 100644
--- 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.ml b/serlib/ser_vernacexpr.ml
index b5a60586..d0c13454 100644
--- 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
index 03b81ab6..d9522d5b 100644
--- a/serlib/ser_vernacexpr.mli
+++ b/serlib/ser_vernacexpr.mli
@@ -104,22 +104,22 @@ 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]
 
-type notation_declaration =
-  [%import: Vernacexpr.notation_declaration]
+type decl_notation =
+  [%import: Vernacexpr.decl_notation]
   [@@deriving sexp,yojson,hash,compare]
 
 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]