diff options
| author | Pierre-Marie Pédrot | 2020-09-03 12:46:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-03 12:46:59 +0200 |
| commit | b3bf44f21581fc72f4087e42a192f15242a545e9 (patch) | |
| tree | a397c05ba649bccc3859a5e16f1140b4ec9e9d16 /proofs | |
| parent | 5ea743ed08f96013438b6ff54b81745e4191d3c6 (diff) | |
| parent | 6f3d15a9edc2e04e973c47ee20093a1f79a990cf (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.ml | 2 |
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; |
