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 5b4a0dccb8..dc8fe35680 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -334,7 +334,7 @@ let evar_define isevars (ev,argsv) rhs = *) let has_undefined_isevars isevars t = - try let _ = whd_ise isevars.evars t in false + try let _ = local_strong (whd_ise isevars.evars) t in false with Uninstantiated_evar _ -> true let head_is_evar isevars = |