- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 174 insertions, 124 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e41bebea11..a4933a8963 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -677,7 +677,7 @@ and my_find_search_nodelta db_list local_db hdc concl =
 	      tclTHEN 
 		(unify_resolve_nodelta (term,cl)) 
 		(trivial_fail_db false db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> 
 	      conclPattern concl (Option.get p) tacast))
     tacl
@@ -717,7 +717,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	      tclTHEN 
 		(unify_resolve st (term,cl)) 
 		(trivial_fail_db true db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> 
 	      conclPattern concl (Option.get p) tacast))
       tacl
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e3e90c7ca6..3be1e45dee 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -17,7 +17,9 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Term
+open Termops
 open Util
+open Rawterm
 open Vernacinterp
 open Tacexpr
 open Mod_subst
@@ -80,7 +82,10 @@ let one_base general_rewrite_maybe_in tac_main bas =
 let autorewrite tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
-       tclTHEN tac (one_base (fun dir -> general_rewrite dir []) tac_main bas)) tclIDTAC lbas))
+       tclTHEN tac
+        (one_base (fun dir -> general_rewrite dir all_occurrences)
+	  tac_main bas))
+      tclIDTAC lbas))
 
 let autorewrite_multi_in idl tac_main lbas : tactic =
   fun gl -> 
@@ -96,7 +101,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic =
       | _ -> (* even the hypothesis id is missing *)
              error ("No such hypothesis : " ^ (string_of_id !id))
     in
-    let gl' = general_rewrite_in dir [] !id cstr false gl in
+    let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
@@ -132,7 +137,9 @@ let gen_auto_multi_rewrite tac_main lbas cl =
   let try_do_hyps treat_id l = 
     autorewrite_multi_in (List.map treat_id l) tac_main lbas
   in 
-  if cl.concl_occs <> [] then 
+  if cl.concl_occs <> all_occurrences_expr &
+     cl.concl_occs <> no_occurrences_expr
+  then 
     error "The \"at\" syntax isn't available yet for the autorewrite tactic"
   else 
     let compose_tac t1 t2 = 
@@ -141,7 +148,7 @@ let gen_auto_multi_rewrite tac_main lbas cl =
 	| _ ->      tclTHENFIRST t1 t2
     in
     compose_tac
-	(if cl.onconcl then autorewrite tac_main lbas else tclIDTAC)
+	(if cl.concl_occs <> no_occurrences_expr then autorewrite tac_main lbas else tclIDTAC)
 	(match cl.onhyps with 
 	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
 	   | None -> 
@@ -153,11 +160,12 @@ let gen_auto_multi_rewrite tac_main lbas cl =
 
 let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC
 
-let auto_multi_rewrite_with tac_main lbas cl gl = 
-  match cl.Tacexpr.onconcl,cl.Tacexpr.onhyps with 
+let auto_multi_rewrite_with tac_main lbas cl gl =
+  let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in
+  match onconcl,cl.Tacexpr.onhyps with 
     | false,Some [_] | true,Some [] | false,Some [] ->   
 	(* autorewrite with .... in clause using tac n'est sur que 
-	   si clause reprensente soit le but soit UNE hypothse 
+	   si clause represente soit le but soit UNE hypothese 
 	*)
 	gen_auto_multi_rewrite tac_main  lbas cl gl
     | _ -> 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bbeeb4e038..37fe7c3c81 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -125,7 +125,7 @@ and e_my_find_search db_list local_db hdc concl =
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (unify_e_resolve st (term,cl)) 
 		(e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> conclPattern concl 
 	      (Option.get p) tacast
       in 
@@ -793,8 +793,10 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
 let default_flags = { under_lambdas = true; on_morphisms = true; }
 
-let build_new gl env sigma flags occs hypinfo concl cstr evars =
-  let is_occ occ = occs = [] || List.mem occ occs in
+let build_new gl env sigma flags loccs hypinfo concl cstr evars =
+  let (nowhere_except_in,occs) = loccs in
+  let is_occ occ = 
+    if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
   let rec aux env t occ cstr =
     let unif = unify_eqn env sigma hypinfo t in
     let occ = if unif = None then occ else succ occ in
@@ -899,7 +901,11 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
 			Some (prf', (car', rel', c1', c2'))
 		in res, occ
 	  | _ -> None, occ
-  in aux env concl 0 cstr
+  in
+  let eq,nbocc_min_1 = aux env concl 0 cstr in
+  let rest = List.filter (fun o -> o > nbocc_min_1) occs in
+  if rest <> [] then error_invalid_occurrence rest;
+  eq
     
 let resolve_typeclass_evars d p env evd onlyargs =
   let pred = 
@@ -924,7 +930,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   let evars = ref (Evd.create_evar_defs Evd.empty) in
   let env = pf_env gl in
   let sigma = project gl in
-  let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars 
+  let eq = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars 
   in
     match eq with  
     | Some (p, (_, _, oldt, newt)) -> 
@@ -993,12 +999,19 @@ let cl_rewrite_clause c left2right occs clause gl =
 open Genarg
 open Extraargs
 
+let occurrences_of = function
+  | n::_ as nl when n < 0 -> (false,List.map abs nl)
+  | nl -> 
+      if List.exists (fun n -> n < 0) nl then
+	error "Illegal negative occurrence number";
+      (true,nl)
+
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None ]
-| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ]
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
+| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
 END
 
 
@@ -1008,7 +1021,7 @@ let clsubstitute o c =
       (fun cl -> 
 	match cl with
 	  | Some ((_,id),_) when is_tac id -> tclIDTAC
-	  | _ -> tclTRY (cl_rewrite_clause c o [] cl))
+	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
 
 TACTIC EXTEND substitute
 | [ "substitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
@@ -1098,15 +1111,15 @@ let _ =
   
 TACTIC EXTEND setoid_rewrite
    [ "setoid_rewrite" orient(o) constr(c) ]
-   -> [ cl_rewrite_clause c o [] None ]
+   -> [ cl_rewrite_clause c o all_occurrences None ]
  | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] ->
-      [ cl_rewrite_clause c o [] (Some (([],id), []))]
+      [ cl_rewrite_clause c o all_occurrences (Some (([],id), []))]
  | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] ->
-      [ cl_rewrite_clause c o occ None]
+      [ cl_rewrite_clause c o (occurrences_of occ) None]
  | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] ->
-      [ cl_rewrite_clause c o occ (Some (([],id), []))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
  | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] ->
-      [ cl_rewrite_clause c o occ (Some (([],id), []))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
 END
 
 (* let solve_obligation lemma =  *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 843554baee..7d2ccbe219 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -261,11 +261,13 @@ let add_destructor_hint local na loc pat pri code =
     (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let match_dpat dp cls gls =
+  let onconcl = cls.concl_occs <> no_occurrences_expr in
   match (cls,dp) with
-    | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
+    | ({onhyps=lo},HypLocation(_,hypd,concld)) when not onconcl ->
         let hl = match lo with
             Some l -> l
-          | None -> List.map (fun id -> (([],id),InHyp)) (pf_ids_of_hyps gls) in
+          | None -> List.map (fun id -> ((all_occurrences_expr,id),InHyp))
+	              (pf_ids_of_hyps gls) in
         if not
           (List.for_all
             (fun ((_,id),hl) ->
@@ -278,7 +280,7 @@ let match_dpat dp cls gls =
               (is_matching concld.d_sort (pf_type_of gls cl)))
             hl)
         then error "No match"
-    | ({onhyps=Some[];onconcl=true},ConclLocation concld) ->
+    | ({onhyps=Some[]},ConclLocation concld) when onconcl ->
         let cl = pf_concl gls in
         if not
           ((is_matching concld.d_typ cl) &
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c6804329b0..3b982b4c08 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -140,7 +140,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve_nodelta (term,cl)) 
 		 (e_trivial_fail_db false db_list local_db)
-	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> conclPattern concl 
 	       (Option.get p) tacast
        in 
@@ -179,7 +179,7 @@ and e_my_find_search_delta db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl)) 
 		 (e_trivial_fail_db true db_list local_db)
-	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> conclPattern concl 
 	       (Option.get p) tacast
        in 
@@ -448,7 +448,7 @@ END
 let autosimpl db cl =
   let unfold_of_elts constr (b, elts) =
     if not b then 
-      List.map (fun c -> [], constr c) elts
+      List.map (fun c -> all_occurrences, constr c) elts
     else []
   in
   let unfolds = List.concat (List.map (fun dbname -> 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b0c5a29ebd..f907b1fd77 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -109,7 +109,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
 	      then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
 	      else error "The term provided does not end with an equation" 
 	  | Some (hdcncl,_) -> 
-	      if occs <> [] then (
+	      if occs <> all_occurrences then (
 		!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
 	      else
 		let hdcncls = string_of_inductive hdcncl in 
@@ -145,10 +145,10 @@ let general_rewrite_in l2r occs id c =
   general_rewrite_ebindings_clause (Some id) l2r occs (c,NoBindings)
 
 let general_multi_rewrite l2r with_evars c cl = 
-  let occs = List.fold_left 
+  let occs_of = on_snd (List.fold_left 
     (fun acc ->
       function ArgArg x -> x :: acc | ArgVar _ -> acc)
-    [] cl.concl_occs
+    [])
   in
   match cl.onhyps with 
     | Some l -> 
@@ -156,24 +156,24 @@ let general_multi_rewrite l2r with_evars c cl =
 	   each of these locations. *)
 	let rec do_hyps = function 
 	  | [] -> tclIDTAC
-	  | ((_,id),_) :: l -> 
-	      tclTHENFIRST
-	        (general_rewrite_ebindings_in l2r occs id c with_evars)
-	        (do_hyps l)
+	  | ((occs,id),_) :: l -> 
+	    tclTHENFIRST
+	      (general_rewrite_ebindings_in l2r (occs_of occs) id c with_evars)
+	      (do_hyps l)
 	in 
-	if not cl.onconcl then do_hyps l else
+	if cl.concl_occs = no_occurrences_expr then do_hyps l else
 	  tclTHENFIRST
-	    (general_rewrite_ebindings l2r occs c with_evars)
-	    (do_hyps l)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars)
+	   (do_hyps l)
     | None -> 
 	(* Otherwise, if we are told to rewrite in all hypothesis via the 
            syntax "* |-", we fail iff all the different rewrites fail *) 
 	let rec do_hyps_atleastonce = function 
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l -> 
-	      tclIFTHENTRYELSEMUST 
-		(general_rewrite_ebindings_in l2r occs id c with_evars) 
-		(do_hyps_atleastonce l)
+	    tclIFTHENTRYELSEMUST 
+	     (general_rewrite_ebindings_in l2r all_occurrences id c with_evars)
+	     (do_hyps_atleastonce l)
 	in 
 	let do_hyps gl = 
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
@@ -182,10 +182,10 @@ let general_multi_rewrite l2r with_evars c cl =
 	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in 
-	  if not cl.onconcl then do_hyps else
-	    tclIFTHENTRYELSEMUST 
-	      (general_rewrite_ebindings l2r occs c with_evars)
-	      do_hyps
+	if cl.concl_occs = no_occurrences_expr then do_hyps else
+	  tclIFTHENTRYELSEMUST 
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars)
+	   do_hyps
 
 let general_multi_multi_rewrite with_evars l cl tac = 
   let do1 l2r c = 
@@ -212,20 +212,22 @@ let general_multi_multi_rewrite with_evars l cl tac =
    to the resolution of the conditions by a given tactic *)
 
 let conditional_rewrite lft2rgt tac (c,bl) = 
-  tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt [] (c,bl) false)
+  tclTHENSFIRSTn
+    (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let rewriteLR_bindings = general_rewrite_bindings true []
-let rewriteRL_bindings = general_rewrite_bindings false []
+let rewriteLR_bindings = general_rewrite_bindings true all_occurrences
+let rewriteRL_bindings = general_rewrite_bindings false all_occurrences
 
-let rewriteLR = general_rewrite true []
-let rewriteRL = general_rewrite false []
+let rewriteLR = general_rewrite true all_occurrences
+let rewriteRL = general_rewrite false all_occurrences
 
-let rewriteLRin_bindings = general_rewrite_bindings_in true []
-let rewriteRLin_bindings = general_rewrite_bindings_in false []
+let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences
+let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences
 
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
-  tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt [] id (c,bl) false)
+  tclTHENSFIRSTn
+    (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
 let rewriteRL_clause = function
@@ -1124,7 +1126,8 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
+  let hl = List.fold_right 
+    (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 19cf1ed56f..acbaca235e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -21,14 +21,15 @@ open Pattern
 open Tacticals
 open Tactics
 open Tacexpr
+open Termops
 open Rawterm
 open Genarg
 (*i*)
 
 val general_rewrite_bindings : 
-  bool -> int list -> constr with_bindings -> evars_flag -> tactic
+  bool -> occurrences -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite : 
-  bool -> int list -> constr -> tactic
+  bool -> occurrences -> constr -> tactic
 
 (* Obsolete, use [general_rewrite_bindings l2r]
 [val rewriteLR_bindings       : constr with_bindings -> tactic]
@@ -42,13 +43,13 @@ val rewriteRL   : constr  -> tactic
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
 val register_general_setoid_rewrite_clause :
-  (identifier option ->
-    bool -> int list -> constr -> new_goals:constr list -> tactic) -> unit
+  (identifier option -> bool ->
+    occurrences -> constr -> new_goals:constr list -> tactic) -> unit
 
 val general_rewrite_bindings_in :
-  bool -> int list -> identifier -> constr with_bindings -> evars_flag -> tactic
+  bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
-  bool -> int list -> identifier -> constr -> evars_flag -> tactic
+  bool -> occurrences -> identifier -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite : 
   bool -> evars_flag -> constr with_ebindings -> clause -> tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index f768e98e47..158cecfc7c 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -288,12 +288,11 @@ let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause =
    Option.map 
      (fun l -> 
 	List.map 
-	  (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp))
+	  (fun id -> ( (all_occurrences_expr,trad_id id) ,Tacexpr.InHyp))
 	  l
      )
      hyps;
-   Tacexpr.onconcl=concl;
-   Tacexpr.concl_occs = []}
+   Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr}
 
 
 let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0a9ed111fc..11ace2abba 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -65,7 +65,8 @@ let h_generalize_gen cl =
   abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl))
     (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
 let h_generalize cl =
-  h_generalize_gen (List.map (fun c -> (([],c),Names.Anonymous)) cl)
+  h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous))
+    cl)
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c)
 let h_let_tac b na c cl =
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index dc8ff2b9cd..98c0c11045 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1806,7 +1806,7 @@ let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl =
      if_output_relation_is_if gl
   with
     Optimize ->
-      !general_rewrite (fst hyp = Left2Right) [] (snd hyp) gl
+      !general_rewrite (fst hyp = Left2Right) all_occurrences (snd hyp) gl
 
 let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
  let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in 
@@ -1825,6 +1825,8 @@ let analyse_hypothesis gl c =
   eqclause,mkApp (equiv, Array.of_list others),c1,c2
 
 let general_s_rewrite lft2rgt occs c ~new_goals gl =
+  if occs <> all_occurrences then
+    warning "Rewriting at selected occurrences not supported";
   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
   if lft2rgt then 
     relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl
@@ -1862,6 +1864,8 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
    gl
 
 let general_s_rewrite_in id lft2rgt occs c ~new_goals gl =
+  if occs <> all_occurrences then
+    warning "Rewriting at selected occurrences not supported";
   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
   if lft2rgt then 
     relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl
@@ -1916,7 +1920,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
       tclTHENS (assert_tac false Anonymous eq)
 	[onLastHyp (fun id ->
           tclTHEN
-            (rewrite_tac dir [] (mkVar id) ~new_goals)
+            (rewrite_tac dir all_occurrences (mkVar id) ~new_goals)
             (clear [id]));
 	 try_prove_eq_tac]
     in
@@ -1928,7 +1932,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
 	  tclTHENS (assert_tac false Anonymous eq)
 	    [onLastHyp (fun id ->
 	      tclTHEN
-		(rewrite_tac false [] (mkVar id) ~new_goals)
+		(rewrite_tac false all_occurrences (mkVar id) ~new_goals)
 		(clear [id]));
 	     try_prove_eq_tac] gl
       
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 1eb0141c67..244e02dd43 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -12,6 +12,7 @@ open Term
 open Proof_type
 open Topconstr
 open Names
+open Termops
 
 type relation =
    { rel_a: constr ;
@@ -40,7 +41,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr
 val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds
 
 val register_replace : (tactic option -> constr -> constr -> tactic) -> unit
-val register_general_rewrite : (bool -> int list -> constr -> tactic) -> unit
+val register_general_rewrite : (bool -> occurrences -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
 
@@ -58,9 +59,10 @@ val setoid_replace_in :
  identifier -> constr option -> constr -> constr -> new_goals:constr list ->
   tactic
 
-val general_s_rewrite : bool -> int list -> constr -> new_goals:constr list -> tactic
+val general_s_rewrite :
+  bool -> occurrences -> constr -> new_goals:constr list -> tactic
 val general_s_rewrite_in :
- identifier -> bool -> int list -> constr -> new_goals:constr list -> tactic
+  identifier -> bool -> occurrences -> constr -> new_goals:constr list -> tactic
 
 val setoid_reflexivity : tactic
 val setoid_symmetry : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20b4abf8a4..2fc6692a8f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -204,7 +204,7 @@ let add_primitive_tactic s tac =
   atomic_mactab := Idmap.add id tac !atomic_mactab
 
 let _ =
-  let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+  let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in
   List.iter
       (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
       [ "red", TacReduce(Red false,nocl);
@@ -610,8 +610,8 @@ let intern_inversion_strength lf ist = function
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist ((occs,id),hl) =
-  ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
+let intern_hyp_location ist (((b,occs),id),hl) =
+  (((b,List.map (intern_or_var ist) occs),intern_hyp ist (skip_metaid id)), hl)
 
 let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[])
@@ -672,10 +672,10 @@ let extract_let_names lrc =
     lrc []
 
 let clause_app f = function
-    { onhyps=None; onconcl=b;concl_occs=nl } ->
-      { onhyps=None; onconcl=b; concl_occs=nl }
-  | { onhyps=Some l; onconcl=b;concl_occs=nl } ->
-      { onhyps=Some(List.map f l); onconcl=b;concl_occs=nl}
+    { onhyps=None; concl_occs=nl } ->
+      { onhyps=None; concl_occs=nl }
+  | { onhyps=Some l; concl_occs=nl } ->
+      { onhyps=Some(List.map f l); concl_occs=nl}
 
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
@@ -783,7 +783,9 @@ let rec intern_atomic lf ist x =
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
   | TacChange (occl,c,cl) ->
       TacChange (Option.map (intern_constr_with_occurrences ist) occl,
-        (if occl = None & cl.onhyps = None & cl.concl_occs = []
+        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+	    (cl.concl_occs = all_occurrences_expr or
+	     cl.concl_occs = no_occurrences_expr)
          then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
 
@@ -1279,13 +1281,15 @@ let interp_evaluable ist env = function
       interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
 
 (* Interprets an hypothesis name *)
+let interp_occurrences ist (b,occs) =
+  (b,interp_int_or_var_list ist occs)
+
 let interp_hyp_location ist gl ((occs,id),hl) =
-  ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl)
+  ((interp_occurrences ist occs,interp_hyp ist gl id),hl)
 
-let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
+let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
   { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol;
-    onconcl=b;
-    concl_occs= interp_int_or_var_list ist occs }
+    concl_occs=interp_occurrences ist occs }
 
 (* Interpretation of constructions *)
 
@@ -1483,22 +1487,23 @@ let pf_interp_type ist gl =
   interp_type ist (project gl) (pf_env gl)
 
 (* Interprets a reduction expression *)
-let interp_unfold ist env (l,qid) =
-  (interp_int_or_var_list ist l,interp_evaluable ist env qid)
+let interp_unfold ist env (occs,qid) =
+  (interp_occurrences ist occs,interp_evaluable ist env qid)
 
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
-let interp_pattern ist sigma env (l,c) = 
-  (interp_int_or_var_list ist l, interp_constr ist sigma env c)
+let interp_pattern ist sigma env (occs,c) = 
+  (interp_occurrences ist occs, interp_constr ist sigma env c)
 
 let pf_interp_constr_with_occurrences ist gl =
   interp_pattern ist (project gl) (pf_env gl)
 
 let pf_interp_constr_with_occurrences_and_name_as_list = 
   pf_interp_constr_in_compound_list
-    (fun c -> (([],c),Anonymous))
-    (function (([],c),Anonymous) -> c | _ -> raise Not_found)
+    (fun c -> ((all_occurrences_expr,c),Anonymous))
+    (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c 
+      | _ -> raise Not_found)
     (fun ist gl (occ_c,na) ->
       (interp_pattern ist (project gl) (pf_env gl) occ_c,
        interp_fresh_name ist gl na))
@@ -2189,7 +2194,9 @@ and interp_atomic ist gl = function
       h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
   | TacChange (occl,c,cl) ->
       h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl)
-        (if occl = None & cl.onhyps = None & cl.concl_occs = []
+        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+	    (cl.concl_occs = all_occurrences_expr or
+	     cl.concl_occs = no_occurrences_expr)
 	 then pf_interp_type ist gl c 
 	 else pf_interp_constr ist gl c)
         (interp_clause ist gl cl)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dd8aa12941..577ef0c6f2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -23,6 +23,7 @@ open Refiner
 open Tacmach
 open Clenv
 open Clenvtac
+open Rawterm
 open Pattern
 open Matching
 open Evar_refiner
@@ -123,17 +124,21 @@ let tclTRY_HYPS (tac : constr->tactic) gl =
 type simple_clause = identifier gsimple_clause
 type clause = identifier gclause
 
-let allClauses = { onhyps=None; onconcl=true; concl_occs=[] }
-let allHyps = { onhyps=None; onconcl=false; concl_occs=[] }
-let onHyp id = { onhyps=Some[(([],id),InHyp)]; onconcl=false; concl_occs=[] }
-let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] }
+let allClauses = { onhyps=None; concl_occs=all_occurrences_expr }
+let allHyps = { onhyps=None; concl_occs=no_occurrences_expr }
+let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr }
+let onHyp id =
+  { onhyps=Some[((all_occurrences_expr,id),InHyp)]; concl_occs=no_occurrences_expr }
 
 let simple_clause_list_of cl gls =
   let hyps =
     match cl.onhyps with 
-        None -> List.map (fun id -> Some(([],id),InHyp)) (pf_ids_of_hyps gls)
-      | Some l -> List.map (fun h -> Some h) l in
-  if cl.onconcl then None::hyps else hyps
+    | None ->
+	let f id = Some((all_occurrences_expr,id),InHyp) in
+	List.map f (pf_ids_of_hyps gls)
+    | Some l ->
+	List.map (fun h -> Some h) l in
+  if cl.concl_occs = all_occurrences_expr then None::hyps else hyps
 
 
 (* OR-branch *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 905511b120..4ec8ee0ae0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -56,6 +56,8 @@ let rec nb_prod x =
       | _ -> n
   in count 0 x
 
+let inj_with_occurrences e = (all_occurrences_expr,e)
+
 let inj_open c = (Evd.empty,c)
 
 let inj_occ (occ,c) = (occ,inj_open c)
@@ -214,7 +216,8 @@ let change_option occl t = function
 
 let change occl c cls =
   (match cls, occl with
-      ({onhyps=(Some(_::_::_)|None)}|{onhyps=Some(_::_);onconcl=true}),
+      ({onhyps=(Some(_::_::_)|None)}
+      |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
       Some _ ->
 	error "No occurrences expected when changing several hypotheses"
     | _ -> ());
@@ -256,8 +259,8 @@ let reduce redexp cl goal =
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr = function 
-  | ConstRef sp -> unfold_in_concl [[],EvalConstRef sp]
-  | VarRef id -> unfold_in_concl [[],EvalVarRef id]
+  | ConstRef sp -> unfold_in_concl [all_occurrences,EvalConstRef sp]
+  | VarRef id -> unfold_in_concl [all_occurrences,EvalVarRef id]
   | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
@@ -1175,7 +1178,7 @@ let generalize_dep c gl =
       | _ -> tothin
   in
   let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let cl'' = generalize_goal gl 0 (([],c),Anonymous) cl' in
+  let cl'' = generalize_goal gl 0 ((all_occurrences,c),Anonymous) cl' in
   let args = Array.to_list (instance_from_named_context to_quantify_rev) in
   tclTHEN
     (apply_type cl'' (c::args))
@@ -1187,7 +1190,8 @@ let generalize_gen lconstr gl =
     list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
   apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl
 
-let generalize l = generalize_gen (List.map (fun c -> (([],c),Anonymous)) l)
+let generalize l =
+  generalize_gen (List.map (fun c -> ((all_occurrences,c),Anonymous)) l)
 
 let revert hyps gl = 
   tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
@@ -1235,14 +1239,15 @@ let out_arg = function
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | ((occs,id'),hl)::_ when id=id' -> Some (List.map out_arg occs)
+    | (((b,occs),id'),hl)::_ when id=id' -> Some (b,List.map out_arg occs)
     | _::l -> hyp_occ l in
   match cls.onhyps with
-      None -> Some []
+      None -> Some (all_occurrences)
     | Some l -> hyp_occ l
 
 let occurrences_of_goal cls =
-  if cls.onconcl then Some (List.map out_arg cls.concl_occs) else None
+  if cls.concl_occs = no_occurrences_expr then None
+  else Some (on_snd (List.map out_arg) cls.concl_occs)
 
 let in_every_hyp cls = (cls.onhyps=None)
 
@@ -1311,7 +1316,7 @@ let letin_abstract id c occs gl =
       | None -> depdecls
       | Some occ ->
           let newdecl = subst_term_occ_decl occ c d in
-          if occ = [] & d = newdecl then
+          if occ = all_occurrences & d = newdecl then
 	    if not (in_every_hyp occs)
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
@@ -2297,8 +2302,6 @@ let recolle_clenv scheme lid elimclause gl =
     (List.rev clauses)
     elimclause
 
-
-
 (* Unification of the goal and the principle applied to meta variables:
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
@@ -2364,7 +2367,7 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
       if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
       thin dephyps; (* clear dependent hyps *)
       (* pattern to make the predicate appear. *)
-      reduce (Pattern (List.map (fun e -> ([],e)) lidcstr)) onConcl;
+      reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl;
       (* FIXME: Tester ca avec un principe dependant et non-dependant *)
       (if isrec then tclTHENFIRSTn else tclTHENLASTn)
        	(tclTHENLIST [ 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index bfb49cba72..0492e296f2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,6 +26,7 @@ open Genarg
 open Tacexpr
 open Nametab
 open Rawterm
+open Termops
 (*i*)
 
 val inj_open : constr -> open_constr
@@ -121,9 +122,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction * cast_kind -> simple_clause -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (int list * constr) option -> constr -> tactic
-val change_in_hyp     : (int list * constr) option -> constr -> hyp_location ->
-  tactic
+val change_in_concl   : (occurrences * constr) option -> constr -> tactic
+val change_in_hyp     : (occurrences * constr) option -> constr -> 
+                        hyp_location -> tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
 val red_option        : simple_clause -> tactic
@@ -137,18 +138,19 @@ val normalise_in_concl : tactic
 val normalise_in_hyp  : hyp_location        -> tactic
 val normalise_option  : simple_clause -> tactic
 val normalise_vm_in_concl : tactic
-val unfold_in_concl   : (int list * evaluable_global_reference) list -> tactic
+val unfold_in_concl   :
+  (occurrences * evaluable_global_reference) list -> tactic
 val unfold_in_hyp     : 
-  (int list * evaluable_global_reference) list -> hyp_location -> tactic
+  (occurrences * evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (int list * evaluable_global_reference) list -> simple_clause
+  (occurrences * evaluable_global_reference) list -> simple_clause
     -> tactic
-val reduce            : red_expr -> clause -> tactic
 val change            :
-  (int list * constr) option -> constr -> clause -> tactic
-
+  (occurrences * constr) option -> constr -> clause -> tactic
+val pattern_option    : 
+  (occurrences * constr) list -> simple_clause -> tactic
+val reduce            : red_expr -> clause -> tactic
 val unfold_constr     : global_reference -> tactic
-val pattern_option  : (int list * constr) list -> simple_clause -> tactic
 
 (*s Modification of the local context. *)
 
@@ -326,9 +328,9 @@ val forward   : tactic option -> intro_pattern_expr -> constr -> tactic
 val letin_tac : bool option -> name -> constr -> clause -> tactic
 val true_cut                    : name -> constr -> tactic
 val assert_tac                  : bool -> name -> constr -> tactic
-val generalize                  : constr list -> tactic
-val generalize_gen              : ((int list * constr) * name) list -> tactic
-val generalize_dep              : constr  -> tactic
+val generalize      : constr list -> tactic
+val generalize_gen  : ((occurrences * constr) * name) list -> tactic
+val generalize_dep  : constr  -> tactic
 
 val tclABSTRACT : identifier option -> tactic -> tactic