Merge PR #9438: Cleanup universe length for inductives in vconv

Ack-by: SkySkimmer
Reviewed-by: ppedrot

3 files changed, 12 insertions, 12 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 02f38e7214..886d6b1feb 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -222,6 +222,10 @@ let lookup_constant kn env =
 let lookup_mind kn env =
   fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
+let mind_context env mind =
+  let mib = lookup_mind mind env in
+  Declareops.inductive_polymorphic_context mib
+
 let lookup_mind_key kn env =
   Mindmap_env.find kn env.env_globals.env_inductives
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8d5bd85b94..a9e0717559 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -246,6 +246,10 @@ val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
    raises [Not_found] if the required path is not found *)
 val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
+(** The universe context associated to the inductive, empty if not
+    polymorphic *)
+val mind_context : env -> MutInd.t -> Univ.AUContext.t
+
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
 val polymorphic_pind : pinductive -> env -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 04a17f7b08..414c443c4e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -88,17 +88,11 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind ((mi,_i) as ind1) , Aind ind2 ->
     if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
-      if Environ.polymorphic_ind ind1 env then
-        let mib = Environ.lookup_mind mi env in
-	let ulen = 
-          match mib.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
-          | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
-          | Declarations.Cumulative_ind cumi -> 
-            Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-        in
+      let ulen = Univ.AUContext.size (Environ.mind_context env mi) in
+      if ulen = 0 then
+        conv_stack env k stk1 stk2 cu
+      else
         match stk1 , stk2 with
-	| [], [] -> assert (Int.equal ulen 0); cu
         | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
           assert (ulen <= nargs args1);
           assert (ulen <= nargs args2);
@@ -110,8 +104,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
           conv_arguments env ~from:ulen k args1 args2
 	    (conv_stack env k stk1' stk2' cu)
         | _, _ -> assert false (* Should not happen if problem is well typed *)
-      else
-	conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | Aid ik1, Aid ik2 ->
     if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then