diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-02 13:48:53 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-02 16:23:15 -0500 |
| commit | 739d8e50b3681491bd82b516dbbba892ac5b424b (patch) | |
| tree | 1df539e5128d1a51f63863ca04def121f5e9591b /pretyping/evarutil.ml | |
| parent | 5a5f2b4253b5834e09f43cb36a81ce6f53cc2da3 (diff) | |
Refresh rigid universes as well, and in 8.4 compatibility mode,
make them rigid to disallow minimization.
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d3d6901b6..b27803bd0 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -715,7 +715,8 @@ let define_pure_evar_as_product evd evk = let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in - let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + let evd1,(dom,u1) = + new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in @@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk = (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else + let status = univ_flexible_alg in let evd3, (rng, srng) = - new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in + new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng |