From 81e7467a3db24887e1d4026ee8441846eb09309a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 18 Oct 2018 14:15:04 +0200
Subject: Only declare univ binders once for mutind

---
 vernac/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3