From fea073c74f98f3fe6728363c0f8142520ac1e50c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 2 Sep 2020 14:42:01 +0200 Subject: 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. --- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 10 +++++----- tactics/equality.ml | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 784322679f..4cec72597a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = { 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; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d969dea19e..39589b2d11 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = { modulo_eta = false; } -let auto_unif_flags ?(allowed_evars = AllowAll) st = +let auto_unif_flags ?(allowed_evars = Evarsolve.AllowAll) st = let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; @@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if cl.cl_strict then let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - AllowFun allowed - else AllowAll - | _ -> AllowAll - with e when CErrors.noncritical e -> AllowAll + Evarsolve.AllowFun allowed + else Evarsolve.AllowAll + | _ -> Evarsolve.AllowAll + with e when CErrors.noncritical e -> Evarsolve.AllowAll in let tac_of_hint = fun (flags, h) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index b4def7bb51..cecb2df8e0 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.AllowAll; 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.AllowFun 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.AllowAll; 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.AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; -- cgit v1.2.3 From cd37a10f9cf5746edf16611d7f833e0e8cf2c5f8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 2 Sep 2020 18:10:37 +0200 Subject: Abstract type for allowed evars --- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 10 +++++----- tactics/equality.ml | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 4cec72597a..369508c2a3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = { 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; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 39589b2d11..96cbbf0ba8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = { modulo_eta = false; } -let auto_unif_flags ?(allowed_evars = Evarsolve.AllowAll) st = +let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st = let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; @@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if cl.cl_strict then let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - Evarsolve.AllowFun allowed - else Evarsolve.AllowAll - | _ -> Evarsolve.AllowAll - with e when CErrors.noncritical e -> Evarsolve.AllowAll + Evarsolve.AllowedEvars.from_pred allowed + else Evarsolve.AllowedEvars.all + | _ -> Evarsolve.AllowedEvars.all + with e when CErrors.noncritical e -> Evarsolve.AllowedEvars.all in let tac_of_hint = fun (flags, h) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index cecb2df8e0..2388085059 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 = Evarsolve.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 = Evarsolve.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 = Evarsolve.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 = Evarsolve.AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; -- cgit v1.2.3