+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no

InType) for  "replace <c1> with  <c2>" and "replace c1"  and partially
for  "autorewrite".   
+ Adding  a  "by  tactic"  optional argument  to "setoid_replace".  
+ Fixing bug #1207
+ Add new test files for syntax change and updating doc.
+ Moving argument tactic extensions from extratactics to extraargs


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

3 files changed, 27 insertions, 11 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 8f880a767..97dfbfb1e 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -21,7 +21,7 @@ and ct_BINDING =
     CT_binding of ct_ID_OR_INT * ct_FORMULA
 and ct_BINDING_LIST =
     CT_binding_list of ct_BINDING list
-and ct_BOOL =
+and t_BOOL =
     CT_false
   | CT_true
 and ct_CASE =
@@ -684,7 +684,7 @@ and ct_TACTIC_COM =
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
-  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
+  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_CLAUSE * ct_TACTIC_OPT
   | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_right of ct_SPEC_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 064d20abd..9c26c0711 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1711,7 +1711,7 @@ and fTACTIC_COM = function
 | CT_replace_with(x1, x2,x3,x4) ->
    fFORMULA x1;
    fFORMULA x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fTACTIC_OPT x4;
    fNODE "replace_with" 4
 | CT_rewrite_lr(x1, x2, x3) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 024cb5991..f2385e7f2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -497,6 +497,8 @@ let xlate_hyp_location =
   | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
+
+
 let xlate_clause cls =
   let hyps_info =
     match cls.onhyps with
@@ -972,22 +974,36 @@ and xlate_tac =
     | TacRight bindl -> CT_right (xlate_bindings bindl)
     | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
     | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
-    | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) ->
+    | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
-	let id_opt = 
-	  match out_gen Extratactics.rawwit_in_arg_hyp id_opt with 
-	  | None -> ctv_ID_OPT_NONE
-	  | Some (_,id) ->   ctf_ID_OPT_SOME (xlate_ident id)
-	in
+	let cl = 
+	  (* J.F. : 18/08/2006 
+	     Hack to coerce the "clause" argument of replace to a real clause 
+	     To be remove if we can reuse the clause grammar entrie defined in g_tactic
+	  *)
+	  let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in 
+	  let cl_as_xlate_arg = 
+	    {cl_as_clause with 
+	       Tacexpr.onhyps = 
+		option_map 
+		  (fun l -> 
+		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
+		  )
+		  cl_as_clause.Tacexpr.onhyps
+	    }
+	  in
+	  cl_as_xlate_arg
+	in 
+	let cl = xlate_clause cl in 
 	let tac_opt = 
-	  match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
+	  match out_gen (Extraargs.rawwit_by_arg_tac) tac_opt with
 	    | None -> CT_coerce_NONE_to_TACTIC_OPT  CT_none
 	    | Some tac ->
 		let tac =  xlate_tactic tac in
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
-	CT_replace_with (c1, c2,id_opt,tac_opt)
+	CT_replace_with (c1, c2,cl,tac_opt)
     | TacRewrite(b,cbindl,cl) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl)