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/record.ml | |
| 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/record.ml')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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} = |