aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/find_subterm.ml2
-rw-r--r--pretyping/locus.ml1
-rw-r--r--pretyping/locusops.ml17
-rw-r--r--pretyping/locusops.mli2
-rw-r--r--pretyping/tacred.ml1
-rw-r--r--pretyping/unification.ml2
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/equality.ml15
-rw-r--r--tactics/ppred.ml1
12 files changed, 31 insertions, 18 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 525ff7fd0f..d17a8e3cc8 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1746,7 +1746,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
let c_interp patvars env sigma =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aa30ed8d2e..f8e5e0759b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1148,7 +1148,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| (id,_,c,cty,evsref,filter,occs)::subst ->
let set_var k =
match occs with
- | Some Locus.AllOccurrences -> mkVar id
+ | Some (Locus.AtLeastOneOccurrence | Locus.AllOccurrences) -> mkVar id
| Some _ -> user_err Pp.(str "Selection of specific occurrences not supported")
| None ->
let evty = set_holes evdref cty subst in
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index b16087031b..d150f8e1cb 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -125,7 +125,7 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
end;
add_subst t subst; incr pos;
(* Check nested matching subterms *)
- if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then
+ if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then
begin nested := true; ignore (subst_below k t); nested := false end;
(* Do the effective substitution *)
Vars.lift k (bywhat ()))
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 37dd120c1a..087a6b9174 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -20,6 +20,7 @@ type 'a or_var =
type 'a occurrences_gen =
| AllOccurrences
+ | AtLeastOneOccurrence
| AllOccurrencesBut of 'a list (** non-empty *)
| NoOccurrences
| OnlyOccurrences of 'a list (** non-empty *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 6b6a3f8a9f..aaa4ce684d 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -19,15 +19,17 @@ let occurrences_map f = function
| AllOccurrencesBut l ->
let l' = f l in
if l' = [] then AllOccurrences else AllOccurrencesBut l'
- | (NoOccurrences|AllOccurrences) as o -> o
+ | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o
let convert_occs = function
+ | AtLeastOneOccurrence -> (false,[])
| AllOccurrences -> (false,[])
| AllOccurrencesBut l -> (false,l)
| NoOccurrences -> (true,[])
| OnlyOccurrences l -> (true,l)
let is_selected occ = function
+ | AtLeastOneOccurrence -> true
| AllOccurrences -> true
| AllOccurrencesBut l -> not (Int.List.mem occ l)
| OnlyOccurrences l -> Int.List.mem occ l
@@ -46,6 +48,11 @@ let is_nowhere = function
| { onhyps=Some[]; concl_occs=NoOccurrences } -> true
| _ -> false
+let is_all_occurrences = function
+ | AtLeastOneOccurrence
+ | AllOccurrences -> true
+ | _ -> false
+
(** Clause conversion functions, parametrized by a hyp enumeration function *)
(** From [clause] to [simple_clause] *)
@@ -61,12 +68,12 @@ let simple_clause_of enum_hyps cl =
List.map Option.make (enum_hyps ())
| Some l ->
List.map (fun ((occs,id),w) ->
- if occs <> AllOccurrences then error_occurrences ();
+ if not (is_all_occurrences occs) then error_occurrences ();
if w = InHypValueOnly then error_body_selection ();
Some id) l in
if cl.concl_occs = NoOccurrences then hyps
else
- if cl.concl_occs <> AllOccurrences then error_occurrences ()
+ if not (is_all_occurrences cl.concl_occs) then error_occurrences ()
else None :: hyps
(** From [clause] to [concrete_clause] *)
@@ -111,7 +118,7 @@ let clause_with_generic_occurrences cls =
List.for_all
(function ((AllOccurrences,_),_) -> true | _ -> false) hyps in
let concl = match cls.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false in
hyps && concl
@@ -122,6 +129,6 @@ let clause_with_generic_context_selection cls =
List.for_all
(function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in
let concl = match cls.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false in
hyps && concl
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index a07c018c32..ac15fe1018 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -21,6 +21,8 @@ val convert_occs : occurrences -> bool * int list
val is_selected : int -> occurrences -> bool
+val is_all_occurrences : 'a occurrences_gen -> bool
+
(** Usual clauses *)
val allHypsAndConcl : 'a clause_expr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2308a541fb..5db571433a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1105,6 +1105,7 @@ let unfoldoccs env sigma (occs,name) c =
| AllOccurrences -> unfold env sigma name c
| OnlyOccurrences l -> unfo true l
| AllOccurrencesBut l -> unfo false l
+ | AtLeastOneOccurrence -> unfo false []
(* Unfold reduction tactic: *)
let unfoldn loccname env sigma c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ac0b58b92b..ce97912b84 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1649,7 +1649,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
match occurrences_of_hyp hyp occs with
| NoOccurrences, InHyp ->
(push_named_context_val d sign,depdecls)
- | AllOccurrences, InHyp as occ ->
+ | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
let occ = if likefirst then LikeFirst else AtOccs occ in
let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f824552705..3b8232d20a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
let try_do_hyps treat_id l =
autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
in
- if cl.concl_occs != AllOccurrences &&
+ if not (Locusops.is_all_occurrences cl.concl_occs) &&
cl.concl_occs != NoOccurrences
then
Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 769e702da1..a8cfc87f9c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
((c,l) : constr with_bindings) with_evars =
- if occs != AllOccurrences then (
+ if not (Locusops.is_all_occurrences occs) then (
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
Proofview.Goal.enter begin fun gl ->
@@ -595,15 +595,16 @@ let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
else check_required_library ["Coq";"Setoids";"Setoid"]
-let check_setoid cl =
+let check_setoid cl =
+ let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in
Option.fold_left
- ( List.fold_left
+ (List.fold_left
(fun b ((occ,_),_) ->
- b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences)
+ b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ)))
)
)
- ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) &&
- (Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences))
+ (not (Locusops.is_all_occurrences concloccs) &&
+ (concloccs <> NoOccurrences))
cl.onhyps
let replace_core clause l2r eq =
@@ -1724,7 +1725,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
tclTHENLIST
((if need_rewrite then
[revert (List.map snd dephyps);
- general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
+ general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp);
(tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
else
[Proofview.tclUNIT ()]) @
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
index dd1bcd4699..d832dc279c 100644
--- a/tactics/ppred.ml
+++ b/tactics/ppred.ml
@@ -6,6 +6,7 @@ open Pputils
let pr_with_occurrences pr keyword (occs,c) =
match occs with
+ | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +")
| AllOccurrences ->
pr c
| NoOccurrences ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:13:25 +0000