Merge pull request #766 from SkySkimmer/template-entry-qvar

Adapt to coq/coq#20178 (cominductive API change)
LPCIC · Feb 6, 2025 · fde097c · fde097c
2 parents 84ca172 + dfaef02
commit fde097c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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