aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarconv.mli4
-rw-r--r--pretyping/evarsolve.ml44
-rw-r--r--pretyping/evarsolve.mli16
-rw-r--r--pretyping/unification.ml11
-rw-r--r--pretyping/unification.mli2
-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
11 files changed, 66 insertions, 39 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a8a3a21f4a..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 = Evarsolve.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 3dc00d195e..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;
- allowed_evars = AllowAll; with_cs = true;
+ allowed_evars = AllowedEvars.all; with_cs = true;
allow_K_at_toplevel = true }
let default_flags env =
@@ -1209,7 +1209,7 @@ let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat =
| Success sigma -> true, sigma
| UnifFailure _ -> false, sigma
-let default_occurrences_selection ?(allowed_evars=AllowAll) ts n =
+let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n =
(default_occurrence_test ~allowed_evars ts,
List.init n (fun _ -> default_occurrence_selection))
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9343be6484..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 : allowed_evars:Evarsolve.allowed_evars -> 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 : ?allowed_evars:Evarsolve.allowed_evars (* By default, all *) ->
+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 9cf1e6fd6f..09e49f3253 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -25,23 +25,46 @@ open Reductionops
open Evarutil
open Pretype_errors
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
+module AllowedEvars = struct
+
+ type t =
+ | AllowAll
+ | AllowFun of (Evar.t -> bool)
+
+ let mem allowed evk =
+ match allowed with
+ | AllowAll -> true
+ | AllowFun f -> f evk
+
+ let remove evk allowed =
+ let allowed = match allowed with
+ | AllowAll -> fun evk' -> not (Evar.equal evk evk')
+ | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
+ in
+ AllowFun allowed
+
+ let all = AllowAll
+
+ let except evars =
+ AllowFun (fun evk -> not (Evar.Set.mem evk evars))
+
+ let from_pred f =
+ AllowFun f
+
+end
type unify_flags = {
modulo_betaiota: bool;
open_ts : TransparentState.t;
closed_ts : TransparentState.t;
subterm_ts : TransparentState.t;
- allowed_evars : allowed_evars;
+ allowed_evars : AllowedEvars.t;
allow_K_at_toplevel : bool;
with_cs : bool
}
-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
type unification_kind =
| TypeUnification
@@ -1464,11 +1487,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 allowed = match flags.allowed_evars with
- | AllowAll -> fun evk' -> not (Evar.equal evk evk')
- | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
- in
- let flags = { flags with allowed_evars = AllowFun allowed } 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 89e162937d..c248e50820 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,9 +16,17 @@ type alias
val of_alias : alias -> EConstr.t
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
+module AllowedEvars : sig
+
+ type t
+
+ val all : t
+ val mem : t -> Evar.t -> bool
+ val remove : Evar.t -> t -> t
+ val except : Evar.Set.t -> t
+ val from_pred : (Evar.t -> bool) -> t
+
+end
type unify_flags = {
modulo_betaiota : bool;
@@ -30,7 +38,7 @@ type unify_flags = {
subterm_ts : TransparentState.t;
(* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
unifications. *)
- allowed_evars : allowed_evars;
+ 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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d63d367a84..746a237b24 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -285,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 *)
@@ -337,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;
@@ -417,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.except @@ Evar.Map.domain undefined
(* Default flags for looking for subterms in elimination tactics *)
(* Not used in practice at the current date, to the exception of *)
@@ -600,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 e3750f7d97..5462e09359 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -22,7 +22,7 @@ type core_unify_flags = {
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
- allowed_evars : Evarsolve.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 65a7a6c711..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 = Evarsolve.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 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;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:51:41 +0000