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 /tactics/equality.ml | |
| 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 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 8a406ce8c5..535725b11d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -105,7 +105,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; 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; @@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause = if Evar.Map.mem evk initial then false else Evar.Set.mem evk (Lazy.force newevars) in - let allowed_evars = AllowFun allowed in + let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in {flags with core_unify_flags = {flags.core_unify_flags with allowed_evars}; merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; @@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; |