Only declare univ binders once for mutind

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 0c39458a57..f405c4d5a9 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -535,11 +535,11 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_, kn), prim = declare_mind mie in
   let mind = Global.mind_of_delta_kn kn in
+  Declare.declare_univ_binders (IndRef (mind,0)) pl;
   List.iteri (fun i (indimpls, constrimpls) ->
               let ind = (mind,i) in
               let gr = IndRef ind in
               maybe_declare_manual_implicits false gr indimpls;
-              Declare.declare_univ_binders gr pl;
               List.iteri
                 (fun j impls ->
                  maybe_declare_manual_implicits false