From a829056747edaf668bb99baf1f95b309e5d90179 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 6 Feb 2025 16:36:21 +0100 Subject: [PATCH] Fix #766 --- src/coq_elpi_HOAS.mli | 6 ++++++ src/coq_elpi_builtins.ml | 9 ++++++++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index ec42fee2b..6bae0d63d 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -110,9 +110,15 @@ val lp2skeleton : type coercion_status = Regular | Off | Reversible type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_canonical : bool } +[%%if coq = "8.20" || coq = "9.0"] +val lp2inductive_entry : + depth:int -> empty coq_context -> constraints -> State.t -> term -> + State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals +[%%else] val lp2inductive_entry : depth:int -> empty coq_context -> constraints -> State.t -> term -> State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals +[%%endif] val inductive_decl2lp : depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * UVars.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) -> diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 33304e29a..2f028113f 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1505,7 +1505,13 @@ It's a fatal error if Name cannot be located.|})), (fun s _ ~depth:_ -> !: (locate_gref s))), DocAbove); ] - + +[%%if coq = "8.20" || coq = "9.0"] +let univ_binder_compat_820 a b = a +[%%else] +let univ_binder_compat_820 a b = b +[%%endif] + let coq_rest_builtins = let open API.BuiltIn in let open Pred in @@ -2101,6 +2107,7 @@ Supported attributes: in let () = global_push_context_set uctx in let mind = + let univ_binders = univ_binder_compat_820 (uentry', ubinders) univ_binders in declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim me univ_binders ind_impls in let ind = mind, 0 in let id, cids = match me.Entries.mind_entry_inds with