aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 65a7a6c711..8e3cab70ea 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -673,7 +673,7 @@ let fail_quick_core_unif_flags = {
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true; (* ? *)
- allowed_evars = Evarsolve.AllowAll;
+ allowed_evars = Evarsolve.AllowedEvars.all;
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = false;
modulo_eta = true;