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

13 files changed, 84 insertions, 79 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bb0d3335c..c82e607d4 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1364,7 +1364,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl -> 
 		  observe_tac 
 		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) 
-		    (tclTRY (Equality.general_rewrite_in true id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true [] id (mkVar eq) false))
 		    gl
 	       ) 
 	       eqs
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 8d9bfdbc5..afe7fc6d2 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -335,7 +335,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		h_intros thin_intros;
 		
 		tclMAP 
-		  (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq false)) 
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) 
 		  (List.rev eqs);
 		(fun g1 -> 
 		   let ty_teq = pf_type_of g1 (mkVar teq) in 
@@ -495,7 +495,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	   Nameops.out_name k_na,Nameops.out_name def_na
 	 in
 	 tclTHENS
-	   (general_rewrite_bindings false
+	   (general_rewrite_bindings false []
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
 				dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -1169,7 +1169,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 		  let _,_,t  = destProd t_eq in let def_na,_,_ = destProd t in 
 		  Nameops.out_name def_na
 		in
-		observe_tac "rewrite heq" (general_rewrite_bindings false
+		observe_tac "rewrite heq" (general_rewrite_bindings false []
 		(mkVar heq2,
 		 ExplicitBindings[dummy_loc,NamedHyp def_id,
 				  f]) false) gls)
@@ -1225,7 +1225,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 			       f_S(mkVar pmax');
 			       dummy_loc, NamedHyp def_id, f])
 			 in
-			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false []
 								       c_b false))
 			     g
 		     )
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 84568588c..66246faf5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -826,9 +826,9 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS
 		 (tclORELSE
-                   (Setoid_replace.general_s_rewrite true c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i
                      ~new_goals:[])
-                   (Setoid_replace.general_s_rewrite false c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i
                      ~new_goals:[]))
                  [tac]))
 	 else
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5e50e9859..522022bb3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -277,6 +277,8 @@ GEXTEND Gram
           {onhyps=Some hl; onconcl=b; concl_occs=occs}
       | "in"; hl=LIST0 hypident_occ SEP"," ->
           {onhyps=Some hl; onconcl=false; concl_occs=[]}
+      | occs=occurrences ->
+	  {onhyps=Some[]; onconcl=true; concl_occs=occs}
       | ->
 	  {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
   ;
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
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 9feac5411..92ca06647 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Tacmach
 open Util
@@ -793,7 +793,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
             (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
                       Auto.default_auto
             ]);
-         Pfedit.by (Equality.general_rewrite_bindings_in true 
+         Pfedit.by (Equality.general_rewrite_bindings_in true []
                               (List.hd !avoid) 
                               ((mkVar (List.hd (List.tl !avoid))),
                                 Rawterm.NoBindings
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 23f26038e..726d26131 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -227,9 +227,6 @@ let dump_universes s =
   with
       e -> close_out output; raise e
 
-let print_instances c =
-  ppnl (Prettyp.print_instances (global c))
-
 (*********************)
 (* "Locate" commands *)
 
@@ -977,7 +974,7 @@ let vernac_print = function
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
   | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
-  | PrintInstances c -> print_instances c 
+  | PrintInstances c -> ppnl (Prettyp.print_instances (global c))
   | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->