diff options
| author | Pierre-Marie Pédrot | 2015-05-12 14:16:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-12 14:22:29 +0200 |
| commit | a49cd60c67aca452500c82aad61327823f9abe31 (patch) | |
| tree | 4b1c3572e20d0e8bade0efa5409b6933d042ae78 | |
| parent | 17f2b11a9a6bb39379239122e77ec12d0b96ff63 (diff) | |
Fixing bug #4234.
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2508f4ef3b..6d076ecd11 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -713,7 +713,7 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = whd_evar evd evi.evar_concl 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 evd2,rng = |