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