locus: Add an AtLeastOneOccurrence constructor.

The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).

3 files changed, 10 insertions, 8 deletions

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 ->