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

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,

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 =

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

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

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

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

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

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 =

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

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.")

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 ()]) @

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