diff options
| author | Pierre-Marie Pédrot | 2020-05-13 14:01:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 16:59:46 +0200 |
| commit | f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 (patch) | |
| tree | 39f979c1f1808034e6bdc15daff247a01d359c0a /vernac | |
| parent | d80458841316ca7edf7317ef412142e27133c931 (diff) | |
Make explicit that UGraph lower bounds are only of two kinds.
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index cc9b840bed..4242f06844 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let indnames = List.map (fun ind -> ind.ind_name) indl in (* 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 env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) = interp_params env0 udecl uparamsl paramsl diff --git a/vernac/record.ml b/vernac/record.ml index 9fda98d08e..36254780cd 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records = any Set <= i constraint for universes that might actually be instantiated with Prop. *) let is_template = List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in - let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in + let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let () = let error bk {CAst.loc; v=name} = |