Fix #766

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)) ->

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