ComInductive: use lbound=Prop iff non polymorphic

This avoids having to interp params and intern arities twice.

2 files changed, 14 insertions, 23 deletions

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 525ca48bee..04514c15cb 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -67,9 +67,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.34} in
-let ff := Type@{UnivBinders.36} in tt -> ff
-     : Type@{max(UnivBinders.33,UnivBinders.35)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+     : Type@{max(UnivBinders.32,UnivBinders.34)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
@@ -142,16 +142,16 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.59} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |=  *)
+axfoo@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |=  *)
 
 axfoo is universe polymorphic
 Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.60} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |=  *)
+axbar@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |=  *)
 
 axbar is universe polymorphic
 Arguments axbar _%type_scope
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d711c9aea0..fdb54ef850 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -433,26 +433,17 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   then user_err (str "Inductives with uniform parameters may not have attached notations.");
 
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-  let sigma, env_params, infos =
+
+  (* In case of template polymorphism, we need to compute more constraints *)
+  let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+
+  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
     interp_params env0 udecl uparamsl paramsl
   in
 
   (* Interpret the arities *)
   let arities = List.map (intern_ind_arity env_params sigma) indl in
 
-  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template =
-    let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in
-    if not poly && is_template then
-      (* In case of template polymorphism, we need to compute more constraints *)
-      let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in
-      let sigma, env_params, infos =
-        interp_params env0 udecl uparamsl paramsl
-      in
-      let arities = List.map (intern_ind_arity env_params sigma) indl in
-      sigma, env_params, infos, arities, is_template
-    else sigma, env_params, infos, arities, is_template
-  in
-
   let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
   let arities, relevances, arityconcl, indimpls = List.split4 arities in