aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml424
-rw-r--r--tactics/equality.ml10
-rw-r--r--tactics/rewrite.ml428
-rw-r--r--tactics/tactics.ml4
5 files changed, 34 insertions, 34 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index afb8121e8..d743135a2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1037,7 +1037,7 @@ let auto_unif_flags = {
resolve_evars = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
+ frozen_evars = Evar.Set.empty;
restrict_conv_on_strict_subterms = false; (* Compat *)
modulo_betaiota = false;
modulo_eta = true;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c62499fdf..ee296c5e5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -71,7 +71,7 @@ let auto_unif_flags = {
resolve_evars = false;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
+ frozen_evars = Evar.Set.empty;
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = true;
modulo_eta = true;
@@ -80,7 +80,7 @@ let auto_unif_flags = {
let rec eq_constr_mod_evars x y =
match kind_of_term x, kind_of_term y with
- | Evar (e1, l1), Evar (e2, l2) when not (Int.equal e1 e2) -> true
+ | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t gl =
@@ -197,7 +197,7 @@ let rec catchable = function
| e -> Logic.catchable_exception e
let nb_empty_evars s =
- ExistentialMap.cardinal (undefined_map s)
+ Evar.Map.cardinal (undefined_map s)
let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
@@ -398,7 +398,7 @@ let isProp env sigma concl =
let needs_backtrack only_classes env evd oev concl =
if Option.is_empty oev || isProp env evd concl then
- not (Int.Set.is_empty (Evarutil.evars_of_term concl))
+ not (Evar.Set.is_empty (Evarutil.evars_of_term concl))
else true
let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
@@ -525,19 +525,19 @@ let resolve_all_evars_once debug limit p evd =
Beware of the imperative effects on the partition structure,
it should not be shared, but only used locally. *)
-module Intpart = Unionfind.Make(Int.Set)(Int.Map)
+module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
let deps_of_constraints cstrs evm p =
List.iter (fun (_, _, x, y) ->
let evx = Evarutil.undefined_evars_of_term evm x in
let evy = Evarutil.undefined_evars_of_term evm y in
- Intpart.union_set (Int.Set.union evx evy) p)
+ Intpart.union_set (Evar.Set.union evx evy) p)
cstrs
let evar_dependencies evm p =
Evd.fold_undefined
(fun ev evi _ ->
- let evars = Int.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+ let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
in Intpart.union_set evars p)
evm ()
@@ -572,7 +572,7 @@ let split_evars evm =
let evars_in_comp comp evm =
try
evars_reset_evd
- (Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
+ (Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
comp Evd.empty) evm
with Not_found -> assert false
@@ -590,7 +590,7 @@ let is_inference_forced p evd ev =
with Not_found -> assert false
let is_mandatory p comp evd =
- Int.Set.exists (is_inference_forced p evd) comp
+ Evar.Set.exists (is_inference_forced p evd) comp
(** In case of unsatisfiable constraints, build a nice error message *)
@@ -630,7 +630,7 @@ let select_and_update_evars p oevd in_comp evd ev evi =
let has_undefined p oevd evd =
let check ev evi = snd (p oevd ev evi) in
- ExistentialMap.exists check (Evd.undefined_map evd)
+ Evar.Map.exists check (Evd.undefined_map evd)
(** Revert the resolvability status of evars after resolution,
potentially unprotecting some evars that were set unresolvable
@@ -655,8 +655,8 @@ let revert_resolvability oevd evd =
exception Unresolved
let resolve_all_evars debug m env p oevd do_split fail =
- let split = if do_split then split_evars oevd else [Int.Set.empty] in
- let in_comp comp ev = if do_split then Int.Set.mem ev comp else true
+ let split = if do_split then split_evars oevd else [Evar.Set.empty] in
+ let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
in
let rec docomp evd = function
| [] -> revert_resolvability oevd evd
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f5ab039b4..d1d4e003d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -105,7 +105,7 @@ let rewrite_unif_flags = {
Unification.resolve_evars = true;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.frozen_evars = ExistentialSet.empty;
+ Unification.frozen_evars = Evar.Set.empty;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
@@ -120,9 +120,9 @@ let freeze_initial_evars sigma flags clause =
let newevars = Evd.collect_evars (clenv_type clause) in
let evars =
fold_undefined (fun evk _ evars ->
- if ExistentialSet.mem evk newevars then evars
- else ExistentialSet.add evk evars)
- sigma ExistentialSet.empty in
+ if Evar.Set.mem evk newevars then evars
+ else Evar.Set.add evk evars)
+ sigma Evar.Set.empty in
{ flags with Unification.frozen_evars = evars }
let make_flags frzevars sigma flags clause =
@@ -178,7 +178,7 @@ let rewrite_conv_closed_unif_flags = {
Unification.use_meta_bound_pattern_unification = true;
- Unification.frozen_evars = ExistentialSet.empty;
+ Unification.frozen_evars = Evar.Set.empty;
(* This is set dynamically *)
Unification.restrict_conv_on_strict_subterms = false;
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 7a135bef0..fa0cb1468 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -134,7 +134,7 @@ let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t =
let evd', t = Evarutil.new_evar evd env t in
- (evd', Int.Set.add (fst (destEvar t)) cstrs), t
+ (evd', Evar.Set.add (fst (destEvar t)) cstrs), t
let new_goal_evar (evd,cstrs) env t =
let evd', t = Evarutil.new_evar evd env t in
@@ -207,7 +207,7 @@ let build_signature evars env m (cstrs : (types * types option) option list)
type hypinfo = {
cl : clausenv;
- ext : Int.Set.t; (* New evars in this clausenv *)
+ ext : Evar.Set.t; (* New evars in this clausenv *)
prf : constr;
car : constr;
rel : constr;
@@ -302,7 +302,7 @@ let rewrite_unif_flags = {
Unification.resolve_evars = false;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.frozen_evars = ExistentialSet.empty;
+ Unification.frozen_evars = Evar.Set.empty;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
@@ -319,7 +319,7 @@ let rewrite2_unif_flags =
Unification.resolve_evars = false;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.frozen_evars = ExistentialSet.empty;
+ Unification.frozen_evars = Evar.Set.empty;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = true;
Unification.modulo_eta = true;
@@ -337,7 +337,7 @@ let general_rewrite_unif_flags () =
Unification.resolve_evars = false;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.frozen_evars = ExistentialSet.empty;
+ Unification.frozen_evars = Evar.Set.empty;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = true;
Unification.modulo_eta = true;
@@ -369,15 +369,15 @@ let solve_remaining_by by env prf =
in { env with evd = evd' }, prf
let extend_evd sigma ext sigma' =
- Int.Set.fold (fun i acc ->
+ Evar.Set.fold (fun i acc ->
Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i)))
ext sigma
let shrink_evd sigma ext =
- Int.Set.fold (fun i acc -> Evd.remove acc i) ext sigma
+ Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma
let no_constraints cstrs =
- fun ev _ -> not (Int.Set.mem ev cstrs)
+ fun ev _ -> not (Evar.Set.mem ev cstrs)
let unify_eqn env (sigma, cstrs) hypinfo by t =
if isEvar t then None
@@ -526,7 +526,7 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
let default_flags = { under_lambdas = true; on_morphisms = true; }
-type evars = evar_map * Int.Set.t (* goal evars, constraint evars *)
+type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
type rewrite_proof =
| RewPrf of constr * constr
@@ -1129,7 +1129,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| None -> (sort, inverse sort impl)
| Some _ -> (sort, impl)
in
- let evars = (sigma, Int.Set.empty) in
+ let evars = (sigma, Evar.Set.empty) in
let eq = apply_strategy strat env avoid concl (Some cstr) evars in
match eq with
| Some (Some (p, (evars, cstrs), car, oldt, newt)) ->
@@ -1141,7 +1141,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
let evars = (* Keep only original evars (potentially instantiated) and goal evars,
the rest has been defined and substituted already. *)
Evd.fold (fun ev evi acc ->
- if Int.Set.mem ev cstrs then Evd.remove acc ev
+ if Evar.Set.mem ev cstrs then Evd.remove acc ev
else acc) evars' evars'
in
let res =
@@ -1759,7 +1759,7 @@ let build_morphism_signature m =
let env = Global.env () in
let m = Constrintern.interp_constr Evd.empty env m in
let t = Typing.type_of env Evd.empty m in
- let evdref = ref (Evd.empty, Int.Set.empty) in
+ let evdref = ref (Evd.empty, Evar.Set.empty) in
let cstrs =
let rec aux t =
match kind_of_term t with
@@ -1790,7 +1790,7 @@ let default_morphism sign m =
let env = Global.env () in
let t = Typing.type_of env Evd.empty m in
let evars, _, sign, cstrs =
- build_signature (Evd.empty, Int.Set.empty) env t (fst sign) (snd sign)
+ build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
in
let morph =
mkApp (Lazy.force proper_type, [| t; sign; m |])
@@ -1916,7 +1916,7 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl =
check_evar_map_of_evars_defs cl'.evd;
let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
- {cl=cl'; ext=Int.Set.empty; prf=(mkRel 1); car=car; rel=rel; l2r=l2r;
+ {cl=cl'; ext=Evar.Set.empty; prf=(mkRel 1); car=car; rel=rel; l2r=l2r;
c1=c1; c2=c2; c=None; abs=Some (prf, prfty); flags = flags}
let get_hyp gl evars (c,l) clause l2r =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a6826b9db..e97b01d38 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1779,8 +1779,8 @@ let default_matching_flags sigma = {
use_pattern_unification = false;
use_meta_bound_pattern_unification = false;
frozen_evars =
- fold_undefined (fun evk _ evars -> ExistentialSet.add evk evars)
- sigma ExistentialSet.empty;
+ fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
+ sigma Evar.Set.empty;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = false;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:47:01 +0000