diff options
| -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 = |