aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/unification.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 648dcee0c8..35543ce24a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -187,7 +187,7 @@ let default_no_delta_unify_flags = {
use_metas_eagerly = true;
modulo_delta = empty_transparent_state;
resolve_evars = false;
- use_evars_pattern_unification = true;
+ use_evars_pattern_unification = false;
}
let use_evars_pattern_unification flags =