aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-03 12:46:59 +0200
committerPierre-Marie Pédrot2020-09-03 12:46:59 +0200
commitb3bf44f21581fc72f4087e42a192f15242a545e9 (patch)
treea397c05ba649bccc3859a5e16f1140b4ec9e9d16 /proofs
parent5ea743ed08f96013438b6ff54b81745e4191d3c6 (diff)
parent6f3d15a9edc2e04e973c47ee20093a1f79a990cf (diff)
Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay them
Reviewed-by: ppedrot
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 db76d08736..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 = AllowAll;
+ allowed_evars = Evarsolve.AllowedEvars.all;
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = false;
modulo_eta = true;