Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.

Uses setoid_rewrite even if rewriting with leibniz if there are
specified occurences, maybe a combination of pattern and rewrite could
be done instead. Correct spelling of occurrences.
Coq does not compile with this patch, the next one will make it compile
again.


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

7 files changed, 72 insertions, 66 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e2ce6baeb..5402e6120 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -80,7 +80,7 @@ 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 general_rewrite tac_main bas)) tclIDTAC lbas))
+       tclTHEN tac (one_base (fun dir -> general_rewrite dir []) tac_main bas)) tclIDTAC lbas))
 
 let autorewrite_multi_in idl tac_main lbas : tactic =
   fun gl -> 
@@ -96,7 +96,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 [] !id cstr false gl in
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 60acd9092..f91845a5c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -84,14 +84,14 @@ let general_s_rewrite_clause = function
 let general_setoid_rewrite_clause = ref general_s_rewrite_clause
 let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 
-let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
+let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
   let ctype = pf_apply get_type_of gl c in 
   (* A delta-reduction would be here too strong, since it would 
      break search for a defined setoid relation in head position. *)
   let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
   let head = if isApp t then fst (destApp t) else t in 
     if relation_table_mem head && l = NoBindings then 
-      !general_setoid_rewrite_clause cls lft2rgt c [] gl
+      !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
     else 
       (* Original code. In particular, [splay_prod] performs delta-reduction. *)
       let env = pf_env gl in
@@ -100,45 +100,51 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
 	match match_with_equation t with
 	  | None -> 
 	      if l = NoBindings
-	      then !general_setoid_rewrite_clause cls lft2rgt c [] 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,_) -> 
-              let hdcncls = string_of_inductive hdcncl in 
-	      let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-              let dir = if cls=None then lft2rgt else not lft2rgt in
-              let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-              let elim =
-		try pf_global gl (id_of_string rwr_thm)
-		with Not_found ->
-		  error ("Cannot find rewrite principle "^rwr_thm)
-              in 
-		try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
-		with e -> 
-		  let eq = build_coq_eq () in
-		    if not (eq_constr eq head) then
-		      try !general_setoid_rewrite_clause cls lft2rgt c [] gl
-		      with _ -> raise e
-		    else raise e
-
+	      if occs <> [] then (
+		!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
+	      else
+		let hdcncls = string_of_inductive hdcncl in 
+		let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+		let dir = if cls=None then lft2rgt else not lft2rgt in
+		let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+		let elim =
+		  try pf_global gl (id_of_string rwr_thm)
+		  with Not_found ->
+		    error ("Cannot find rewrite principle "^rwr_thm)
+		in 
+		  try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+		  with e -> 
+		    let eq = build_coq_eq () in
+		      if not (eq_constr eq head) then
+			try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+			with _ -> raise e
+		      else raise e
+			
 let general_rewrite_ebindings = 
   general_rewrite_ebindings_clause None
-let general_rewrite_bindings l2r (c,bl) = 
-  general_rewrite_ebindings_clause None l2r (c,inj_ebindings bl)
+let general_rewrite_bindings l2r occs (c,bl) = 
+  general_rewrite_ebindings_clause None l2r occs (c,inj_ebindings bl)
 
-let general_rewrite l2r c =
-  general_rewrite_bindings l2r (c,NoBindings) false
+let general_rewrite l2r occs c =
+  general_rewrite_bindings l2r occs (c,NoBindings) false
 
-let general_rewrite_ebindings_in l2r id =
-  general_rewrite_ebindings_clause (Some id) l2r
-let general_rewrite_bindings_in l2r id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r (c,inj_ebindings bl)
-let general_rewrite_in l2r id c = 
-  general_rewrite_ebindings_clause (Some id) l2r (c,NoBindings)
+let general_rewrite_ebindings_in l2r occs id =
+  general_rewrite_ebindings_clause (Some id) l2r occs
+let general_rewrite_bindings_in l2r occs id (c,bl) =
+  general_rewrite_ebindings_clause (Some id) l2r occs (c,inj_ebindings bl)
+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 = 
-  if cl.concl_occs <> [] then 
-    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
-  else match cl.onhyps with 
+  let occs = List.fold_left 
+    (fun acc ->
+      function ArgArg x -> x :: acc | ArgVar _ -> acc)
+    [] cl.concl_occs
+  in
+  match cl.onhyps with 
     | Some l -> 
 	(* If a precise list of locations is given, success is mandatory for
 	   each of these locations. *)
@@ -146,12 +152,12 @@ let general_multi_rewrite l2r with_evars c cl =
 	  | [] -> tclIDTAC
 	  | ((_,id),_) :: l -> 
 	      tclTHENFIRST
-	        (general_rewrite_ebindings_in l2r id c with_evars)
+	        (general_rewrite_ebindings_in l2r occs id c with_evars)
 	        (do_hyps l)
 	in 
 	if not cl.onconcl then do_hyps l else
 	  tclTHENFIRST
-	    (general_rewrite_ebindings l2r c with_evars)
+	    (general_rewrite_ebindings l2r occs c with_evars)
 	    (do_hyps l)
     | None -> 
 	(* Otherwise, if we are told to rewrite in all hypothesis via the 
@@ -160,7 +166,7 @@ let general_multi_rewrite l2r with_evars c cl =
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l -> 
 	      tclIFTHENTRYELSEMUST 
-		(general_rewrite_ebindings_in l2r id c with_evars) 
+		(general_rewrite_ebindings_in l2r occs id c with_evars) 
 		(do_hyps_atleastonce l)
 	in 
 	let do_hyps gl = 
@@ -172,7 +178,7 @@ let general_multi_rewrite l2r with_evars c cl =
 	in 
 	  if not cl.onconcl then do_hyps else
 	    tclIFTHENTRYELSEMUST 
-	      (general_rewrite_ebindings l2r c with_evars)
+	      (general_rewrite_ebindings l2r occs c with_evars)
 	      do_hyps
 
 let general_multi_multi_rewrite with_evars l cl tac = 
@@ -200,20 +206,20 @@ 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 [] (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 []
+let rewriteRL_bindings = general_rewrite_bindings false []
 
-let rewriteLR = general_rewrite true
-let rewriteRL = general_rewrite false
+let rewriteLR = general_rewrite true []
+let rewriteRL = general_rewrite false []
 
-let rewriteLRin_bindings = general_rewrite_bindings_in true
-let rewriteRLin_bindings = general_rewrite_bindings_in false
+let rewriteLRin_bindings = general_rewrite_bindings_in true []
+let rewriteRLin_bindings = general_rewrite_bindings_in false []
 
 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 [] id (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
 let rewriteRL_clause = function
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 91a0d33c6..19cf1ed56 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -26,9 +26,9 @@ open Genarg
 (*i*)
 
 val general_rewrite_bindings : 
-  bool -> constr with_bindings -> evars_flag -> tactic
+  bool -> int list -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite : 
-  bool -> constr -> tactic
+  bool -> int list -> constr -> tactic
 
 (* Obsolete, use [general_rewrite_bindings l2r]
 [val rewriteLR_bindings       : constr with_bindings -> tactic]
@@ -43,12 +43,12 @@ val rewriteRL   : constr  -> tactic
 
 val register_general_setoid_rewrite_clause :
   (identifier option ->
-    bool -> constr -> new_goals:constr list -> tactic) -> unit
+    bool -> int list -> constr -> new_goals:constr list -> tactic) -> unit
 
 val general_rewrite_bindings_in :
-  bool -> identifier -> constr with_bindings -> evars_flag -> tactic
+  bool -> int list -> identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
-  bool -> identifier -> constr -> evars_flag -> tactic
+  bool -> int list -> 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 1d9d5e0e9..3124e10a0 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -33,14 +33,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
-let pr_occurences _prc _prlc _prt l =
+let pr_occurrences _prc _prlc _prt l =
   let rec aux = function
     | i :: l -> Pp.int i ++ Pp.spc () ++ aux l
     | [] -> Pp.mt()
   in aux l
 
-ARGUMENT EXTEND occurences TYPED AS int list PRINTED BY pr_occurences
-| [ integer(i) occurences(l) ] -> [ i :: l ]
+ARGUMENT EXTEND occurrences TYPED AS int list PRINTED BY pr_occurrences
+| [ integer(i) occurrences(l) ] -> [ i :: l ]
 | [ ] -> [ [] ]
 END
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index ead64ac3b..f5813e40b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -19,9 +19,9 @@ val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
-val rawwit_occurences : (int list) raw_abstract_argument_type
-val wit_occurences : (int list) typed_abstract_argument_type
-val occurences : (int list) Pcoq.Gram.Entry.e
+val rawwit_occurrences : (int list) raw_abstract_argument_type
+val wit_occurrences : (int list) typed_abstract_argument_type
+val occurrences : (int list) Pcoq.Gram.Entry.e
 
 val rawwit_morphism_signature :
  Setoid_replace.morphism_signature raw_abstract_argument_type
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1b3f4d21b..9f8821341 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) [] (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 
@@ -1824,7 +1824,7 @@ let analyse_hypothesis gl c =
  let others,(c1,c2) = split_last_two args in
   eqclause,mkApp (equiv, Array.of_list others),c1,c2
 
-let general_s_rewrite lft2rgt c ~new_goals gl =
+let general_s_rewrite lft2rgt occs c ~new_goals gl =
   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
   if lft2rgt then 
     relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl
@@ -1861,7 +1861,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
             (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma))))
    gl
 
-let general_s_rewrite_in id lft2rgt c ~new_goals gl =
+let general_s_rewrite_in id lft2rgt occs c ~new_goals gl =
   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 +1916,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 [] (mkVar id) ~new_goals)
             (clear [id]));
 	 try_prove_eq_tac]
     in
@@ -1928,7 +1928,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 [] (mkVar id) ~new_goals)
 		(clear [id]));
 	     try_prove_eq_tac] gl
       
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 2dd153b3f..1eb0141c6 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -40,7 +40,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 -> constr -> tactic) -> unit
+val register_general_rewrite : (bool -> int list -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
 
@@ -58,9 +58,9 @@ val setoid_replace_in :
  identifier -> constr option -> constr -> constr -> new_goals:constr list ->
   tactic
 
-val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic
+val general_s_rewrite : bool -> int list -> constr -> new_goals:constr list -> tactic
 val general_s_rewrite_in :
- identifier -> bool -> constr -> new_goals:constr list -> tactic
+ identifier -> bool -> int list -> constr -> new_goals:constr list -> tactic
 
 val setoid_reflexivity : tactic
 val setoid_symmetry : tactic