aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh6
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--pretyping/evarconv.ml47
-rw-r--r--pretyping/evarconv.mli4
-rw-r--r--pretyping/evarsolve.ml54
-rw-r--r--pretyping/evarsolve.mli28
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/unification.mli6
-rw-r--r--proofs/clenv.ml2
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml10
-rw-r--r--tactics/equality.ml8
12 files changed, 116 insertions, 68 deletions
diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
new file mode 100644
index 0000000000..ee75944a52
--- /dev/null
+++ b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then
+
+ equations_CI_REF=delay-frozen-evarconv
+ equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fb149071c9..a1dbf9a439 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -546,7 +546,7 @@ let rewrite_core_unif_flags = {
Unification.check_applied_meta_types = true;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.allowed_evars = Unification.AllowAll;
+ Unification.allowed_evars = Evarsolve.AllowedEvars.all;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 489e8de602..61453ff214 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full
let default_flags_of ?(subterm_ts=TransparentState.empty) ts =
{ modulo_betaiota = true;
open_ts = ts; closed_ts = ts; subterm_ts;
- frozen_evars = Evar.Set.empty; with_cs = true;
+ allowed_evars = AllowedEvars.all; with_cs = true;
allow_K_at_toplevel = true }
let default_flags env =
@@ -118,8 +118,6 @@ type flex_kind_of_term =
| MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
| Flexible of EConstr.existential
-let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars
-
let flex_kind_of_term flags env evd c sk =
match EConstr.kind evd c with
| LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
@@ -128,8 +126,7 @@ let flex_kind_of_term flags env evd c sk =
if flags.modulo_betaiota then MaybeFlexible c
else Rigid
| Evar ev ->
- if is_frozen flags ev then Rigid
- else Flexible ev
+ if is_evar_allowed flags (fst ev) then Flexible ev else Rigid
| Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid
| Meta _ -> Rigid
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
@@ -192,11 +189,11 @@ let occur_rigidly flags env evd (evk,_) t =
| Rigid _ as res -> res
| Normal b -> Reducible
| Reducible -> Reducible)
- | Evar (evk',l as ev) ->
+ | Evar (evk',l) ->
if Evar.equal evk evk' then Rigid true
- else if is_frozen flags ev then
- Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
- else Reducible
+ else if is_evar_allowed flags evk' then
+ Reducible
+ else Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
| Cast (p, _, _) -> aux p
| Lambda (na, t, b) -> aux b
| LetIn (na, _, _, b) -> aux b
@@ -458,7 +455,7 @@ let conv_fun f flags on_types =
let typefn env evd pbty term1 term2 =
let flags = { (default_flags env) with
with_cs = flags.with_cs;
- frozen_evars = flags.frozen_evars }
+ allowed_evars = flags.allowed_evars }
in f flags env evd pbty term1 term2
in
let termfn env evd pbty term1 term2 =
@@ -500,7 +497,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
(whd_nored_state env evd (term2,Stack.empty))
in
begin match EConstr.kind evd term1, EConstr.kind evd term2 with
- | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+ | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem true pbty,ev,term2) with
| UnifFailure (_,(OccurCheck _ | NotClean _)) ->
@@ -511,7 +508,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
Miller patterns *)
default ()
| x -> x)
- | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+ | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem false pbty,ev,term1) with
| UnifFailure (_, (OccurCheck _ | NotClean _)) ->
@@ -1206,14 +1203,14 @@ type occurrences_selection =
let default_occurrence_selection = Unspecified Abstraction.Imitate
-let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat =
- let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in
+let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat =
+ let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in
match evar_conv_x flags env sigma CONV c pat with
| Success sigma -> true, sigma
| UnifFailure _ -> false, sigma
-let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n =
- (default_occurrence_test ~frozen_evars ts,
+let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n =
+ (default_occurrence_test ~allowed_evars ts,
List.init n (fun _ -> default_occurrence_selection))
let apply_on_subterm env evd fixedref f test c t =
@@ -1554,7 +1551,7 @@ let second_order_matching_with_args flags env evd with_ho pbty ev l t =
if with_ho then
let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in
let argoccs = default_evar_selection flags evd ev in
- let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in
+ let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in
let evd, b =
try second_order_matching flags env evd ev (test,argoccs) t
with PretypeError (_, _, NoOccurrenceFound _) -> evd, false
@@ -1582,8 +1579,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match EConstr.kind evd term1, EConstr.kind evd term2 with
- | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty
- && not (is_frozen flags ev1)
+ | Evar (evk1,args1), (Rel _|Var _) when app_empty
+ && is_evar_allowed flags evk1
&& List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
(remove_instance_local_defs evd evk1 args1) ->
(* The typical kind of constraint coming from pattern-matching return
@@ -1593,8 +1590,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
| None ->
let reason = ProblemBeyondCapabilities in
UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
- | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty
- && not (is_frozen flags ev2)
+ | (Rel _|Var _), Evar (evk2,args2) when app_empty
+ && is_evar_allowed flags evk2
&& List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
(remove_instance_local_defs evd evk2 args2) ->
(* The typical kind of constraint coming from pattern-matching return
@@ -1620,24 +1617,24 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
(evar_define evar_unify flags ~choose:true)
evar_unify flags env evd
(position_problem true pbty) ev1 ev2)
- | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->
+ | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
(* and otherwise second-order matching *)
ise_try evd
[(fun evd -> first_order_unification flags env evd (ev1,l1) appr2);
(fun evd ->
second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)]
- | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 ->
+ | _,Evar ev2 when is_evar_allowed flags (fst ev2) && Array.length l2 <= Array.length l1 ->
(* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
(* and otherwise second-order matching *)
ise_try evd
[(fun evd -> first_order_unification flags env evd (ev2,l2) appr1);
(fun evd ->
second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)]
- | Evar ev1,_ when not (is_frozen flags ev1) ->
+ | Evar ev1,_ when is_evar_allowed flags (fst ev1) ->
(* Try second-order pattern-matching *)
second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2
- | _,Evar ev2 when not (is_frozen flags ev2) ->
+ | _,Evar ev2 when is_evar_allowed flags (fst ev2) ->
(* Try second-order pattern-matching *)
second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1
| _ ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 767a173131..a5a8d1f916 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection
type occurrences_selection =
occurrence_match_test * occurrence_selection list
-val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test
+val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
(** [default_occurrence_selection n]
Gives the default test and occurrences for [n] arguments *)
-val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) ->
+val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) ->
TransparentState.t -> int -> occurrences_selection
val second_order_matching : unify_flags -> env -> evar_map ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 989fb05c3d..4d5715a391 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -25,14 +25,43 @@ open Reductionops
open Evarutil
open Pretype_errors
+module AllowedEvars = struct
+
+ type t =
+ | AllowAll
+ | AllowFun of (Evar.t -> bool) * Evar.Set.t
+
+ let mem allowed evk =
+ match allowed with
+ | AllowAll -> true
+ | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except)
+
+ let remove evk = function
+ | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk)
+ | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except)
+
+ let all = AllowAll
+
+ let except evars =
+ AllowFun ((fun _ -> true), evars)
+
+ let from_pred f =
+ AllowFun (f, Evar.Set.empty)
+
+end
+
type unify_flags = {
modulo_betaiota: bool;
open_ts : TransparentState.t;
closed_ts : TransparentState.t;
subterm_ts : TransparentState.t;
- frozen_evars : Evar.Set.t;
+ allowed_evars : AllowedEvars.t;
allow_K_at_toplevel : bool;
- with_cs : bool }
+ with_cs : bool
+}
+
+let is_evar_allowed flags evk =
+ AllowedEvars.mem flags.allowed_evars evk
type unification_kind =
| TypeUnification
@@ -1307,24 +1336,24 @@ let preferred_orientation evd evk1 evk2 =
let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let aliases = make_alias_map env evd in
- let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in
- let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in
+ let allowed_ev1 = is_evar_allowed flags evk1 in
+ let allowed_ev2 = is_evar_allowed flags evk2 in
if preferred_orientation evd evk1 evk2 then
- try if not frozen_ev1 then
+ try if allowed_ev1 then
solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
else raise (CannotProject (evd,ev2))
with CannotProject (evd,ev2) ->
- try if not frozen_ev2 then
+ try if allowed_ev2 then
solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
else raise (CannotProject (evd,ev1))
with CannotProject (evd,ev1) ->
add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
else
- try if not frozen_ev2 then
+ try if allowed_ev2 then
solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
else raise (CannotProject (evd,ev1))
with CannotProject (evd,ev1) ->
- try if not frozen_ev1 then
+ try if allowed_ev1 then
solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
else raise (CannotProject (evd,ev2))
with CannotProject (evd,ev2) ->
@@ -1390,15 +1419,15 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
let candidates = filter_candidates evd evk untypedfilter NoUpdate in
let filter = closure_of_filter evd evk untypedfilter in
let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
- let frozen = Evar.Set.mem evk flags.frozen_evars in
- if Evar.equal (fst ev1) evk && (frozen || can_drop) then
+ let allowed = is_evar_allowed flags evk in
+ if Evar.equal (fst ev1) evk && (not allowed || can_drop) then
(* No refinement needed *) evd'
else
(* either progress, or not allowed to drop, e.g. to preserve possibly *)
(* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
(* if e can depend on x until ?y is not resolved, or, conversely, we *)
(* don't know if ?y has to be unified with ?y, until e is resolved *)
- if frozen then
+ if not allowed then
(* We cannot prune a frozen evar *)
add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd
else
@@ -1455,7 +1484,8 @@ let occur_evar_upto_types sigma n c =
let instantiate_evar unify flags env evd evk body =
(* Check instance freezing the evar to be defined, as
checking could involve the same evar definition problem again otherwise *)
- let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
+ let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in
+ let flags = { flags with allowed_evars } in
let evd' = check_evar_instance unify flags env evd evk body in
Evd.define evk body evd'
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3fb80432ad..8ff2d7fc63 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,28 @@ type alias
val of_alias : alias -> EConstr.t
+module AllowedEvars : sig
+
+ type t
+ (** Represents the set of evars that can be defined by the pretyper *)
+
+ val all : t
+ (** All evars can be defined *)
+
+ val mem : t -> Evar.t -> bool
+ (** [mem allowed evk] is true iff evk can be defined *)
+
+ val from_pred : (Evar.t -> bool) -> t
+ (** [from_pred p] means evars satisfying p can be defined *)
+
+ val except : Evar.Set.t -> t
+ (** [except evars] means all evars can be defined except the ones in [evars] *)
+
+ val remove : Evar.t -> t -> t
+ (** [remove evk allowed] removes [evk] from the set of evars allowed by [allowed] *)
+
+end
+
type unify_flags = {
modulo_betaiota : bool;
(* Enable beta-iota reductions during unification *)
@@ -26,8 +48,8 @@ type unify_flags = {
subterm_ts : TransparentState.t;
(* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
unifications. *)
- frozen_evars : Evar.Set.t;
- (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *)
+ allowed_evars : AllowedEvars.t;
+ (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *)
allow_K_at_toplevel : bool;
(* During higher-order unifications, allow to produce K-redexes: i.e. to produce
an abstraction for an unused argument *)
@@ -41,6 +63,8 @@ type unification_result =
val is_success : unification_result -> bool
+val is_evar_allowed : unify_flags -> Evar.t -> bool
+
(** Replace the vars and rels that are aliases to other vars and rels by
their representative that is most ancient in the context *)
val expand_vars_in_term : env -> evar_map -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a26c981cb9..207a03d80f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -252,10 +252,6 @@ let unify_r2l x = x
let sort_eqns = unify_r2l
*)
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
(* What this flag controls was activated with all constants transparent, *)
@@ -289,7 +285,7 @@ type core_unify_flags = {
(* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
(* when ?B is a Meta. *)
- allowed_evars : allowed_evars;
+ allowed_evars : AllowedEvars.t;
(* Evars that are allowed to be instantiated *)
(* Useful e.g. for autorewrite *)
@@ -341,7 +337,7 @@ let default_core_unify_flags () =
check_applied_meta_types = true;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
- allowed_evars = AllowAll;
+ allowed_evars = AllowedEvars.all;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = true;
modulo_eta = true;
@@ -421,7 +417,7 @@ let default_no_delta_unify_flags ts =
let allow_new_evars sigma =
let undefined = Evd.undefined_map sigma in
- AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
+ AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined))
(* Default flags for looking for subterms in elimination tactics *)
(* Not used in practice at the current date, to the exception of *)
@@ -604,9 +600,8 @@ let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
ts env sigma (c, Stack.empty))
-let is_evar_allowed flags evk = match flags.allowed_evars with
-| AllowAll -> true
-| AllowFun f -> f evk
+let is_evar_allowed flags evk =
+ AllowedEvars.mem flags.allowed_evars evk
let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
| Evar (evk,_) -> is_evar_allowed flags evk
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f9a969a253..5462e09359 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,10 +13,6 @@ open EConstr
open Environ
open Evd
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
@@ -26,7 +22,7 @@ type core_unify_flags = {
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
- allowed_evars : allowed_evars;
+ allowed_evars : Evarsolve.AllowedEvars.t;
restrict_conv_on_strict_subterms : bool;
modulo_betaiota : bool;
modulo_eta : bool;
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;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 784322679f..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 = 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 d969dea19e..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 = 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
- AllowFun allowed
- else AllowAll
- | _ -> AllowAll
- with e when CErrors.noncritical e -> 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 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;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:49:28 +0000