diff options
| author | Pierre-Marie Pédrot | 2015-05-13 12:54:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-13 12:54:07 +0200 |
| commit | f86b7d3b8cb23e2fc19a936accb421bfdbf2cb4d (patch) | |
| tree | f62409484739c702666cd6a2a0d78d3c15a062b9 | |
| parent | c5d9f483a48265941720afafd5952a917d80204b (diff) | |
Fix for a second avatar of bug #4234.
| -rw-r--r-- | pretyping/evarutil.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6d076ecd11..ee6bbe7fbe 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -795,8 +795,10 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in + let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s + Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) |