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 19b05682f2..9761561a89 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1296,7 +1296,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) let evd = evar_define ~choose env ev1 t2 evd in let evi = Evd.find evd evk1 in if occur_existential evd evi.evar_concl then - let evenv = evar_env evi in + let evenv = evar_unfiltered_env evi in let evc = nf_isevar evd evi.evar_concl in match evi.evar_body with | Evar_defined body -> |