diff options
| author | Maxime Dénès | 2020-09-02 14:42:01 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-02 21:50:13 +0200 |
| commit | fea073c74f98f3fe6728363c0f8142520ac1e50c (patch) | |
| tree | 67402c5ba7e70695028502b810a42ecc400de2fc /proofs/clenv.ml | |
| parent | e9b64e2f09d2a8dcc2558a9ea34268b4d78fdc66 (diff) | |
Replace `frozen` by `allowed` evars in evarconv, and delay them
This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.
Diffstat (limited to 'proofs/clenv.ml')
| -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..65a7a6c711 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.AllowAll; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; |