From 746a13475db79ed7f2c46abc11e44f806af18a7c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 Oct 2024 20:59:44 +0200 Subject: [PATCH 1/2] Adapt to Coq PR #19301 - proof_expr is generalized into body_expr - definition_expr subsumes fixpoint_expr_gen --- serlib/ser_vernacexpr.ml | 12 ++++-------- serlib/ser_vernacexpr.mli | 12 ++++-------- 2 files changed, 8 insertions(+), 16 deletions(-) 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..9a2520d8 100644 --- a/serlib/ser_vernacexpr.mli +++ b/serlib/ser_vernacexpr.mli @@ -104,6 +104,10 @@ 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] @@ -116,10 +120,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] @@ -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] From 9da9f979314a51103e03aa7c21e12f3e8ddbff66 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 27 Oct 2024 14:05:48 +0100 Subject: [PATCH 2/2] Adapt to Coq PR #19301, continued - ident_decl -> decl_ident - notation_declaration -> decl_notation --- serlib/ser_constrexpr.mli | 4 ++-- serlib/ser_vernacexpr.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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.mli b/serlib/ser_vernacexpr.mli index 9a2520d8..d9522d5b 100644 --- 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 =