diff options
| -rw-r--r-- | test-suite/output/UnivBinders.out | 18 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 19 |
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 85f2bf3708..edb03a5c89 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 |