From dfaef026bb48ecfa6912648e43d62c70be224fc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 3 Feb 2025 16:04:56 +0100 Subject: [PATCH] Adapt to coq/coq#20178 (cominductive API change) --- src/coq_elpi_HOAS.mli | 2 +- src/coq_elpi_builtins.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index 4418a7d73..ec42fee2b 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -112,7 +112,7 @@ type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_cano 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 + 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 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 b92217bf6..33304e29a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2101,7 +2101,7 @@ Supported attributes: in let () = global_push_context_set uctx in let mind = - declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim me (uentry', ubinders) ind_impls 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 | [ { Entries.mind_entry_typename = id; mind_entry_consnames = cids }] -> id, cids