Portage d'AutoRewrite

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

8 files changed, 24 insertions, 9 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 028fe1530..dabe5cb00 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -398,7 +398,7 @@ let ast_of_cvt_arg = function
 	     (ast_of_cvt_bind
 		(ast_of_constr false (Global.env ()))) bl)
   | Tacexp ast      -> ope ("TACTIC",[ast])
-  | Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac"
+  | Tac (tac,ast) -> ast
   | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
   | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
                                       (num n); 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index ac1346409..e1cc05873 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -94,7 +94,7 @@ and tactic_arg =
   | Cbindings      of constr   substitution 
   | Quoted_string  of string
   | Tacexp         of Coqast.t
-  | Tac            of tactic
+  | Tac            of tactic * Coqast.t
   | Redexp         of Tacred.red_expr
   | Fixexp         of identifier * int * Coqast.t
   | Cofixexp       of identifier * Coqast.t
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index cc64be716..1c1b66077 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -97,7 +97,7 @@ and tactic_arg =
   | Cbindings      of constr   substitution 
   | Quoted_string  of string
   | Tacexp         of Coqast.t
-  | Tac            of tactic
+  | Tac            of tactic * Coqast.t
   | Redexp         of Tacred.red_expr
   | Fixexp         of identifier * int * Coqast.t
   | Cofixexp       of identifier * Coqast.t
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 53304fe37..840d24b41 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -361,9 +361,12 @@ let tclTHEN_i tac1 tac2 = tclTHENSi tac1 [] tac2;;
 let tclTHENS tac1 tac2l =
   tclTHENSi tac1 tac2l (fun _ -> tclFAIL_s "Wrong number of tactics.");;
 
-(* Same as [tclTHENS] but completes with [Idtac] if the number resulting 
-  subgoals is strictly less than [n] *)
-let tclTHENSI tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclIDTAC);;
+(* Same as [tclTHENS] but completes with [tac3] if the number resulting 
+   subgoals is strictly less than [n] *)
+let tclTHENST tac1 tac2l tac3 = tclTHENSi tac1 tac2l (fun _ -> tac3)
+
+(* Same as tclTHENST but completes with [Idtac] *)
+let tclTHENSI tac1 tac2l = tclTHENST tac1 tac2l tclIDTAC
 
 (* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the last resulting subgoal *)
@@ -477,6 +480,10 @@ let rec tclREPEAT t g =
 
 let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
+(* Repeat on the first subgoal *)
+let rec tclREPEAT_MAIN t g =
+  (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else
+    tclIDTAC)) tclIDTAC) g
 
 (*s Tactics handling a list of goals. *)
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 47d44a9f1..68767dc8c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -59,8 +59,11 @@ val tclTHENL         : tactic -> tactic -> tactic
    an error if the number of resulting subgoals is not [n] *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(* Same as [tclTHENS] but completes with [Idtac] if the number resulting 
-  subgoals is strictly less than [n] *)
+(* Same as [tclTHENS] but completes with [tac3] if the number resulting 
+   subgoals is strictly less than [n] *)
+val tclTHENST        : tactic -> tactic list -> tactic -> tactic
+
+(* Same as tclTHENST but completes with [Idtac] *)
 val tclTHENSI        : tactic -> tactic list -> tactic
 
 (* A special exception for levels for the Fail tactic *)
@@ -68,6 +71,7 @@ exception FailError of int
 
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
+val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index e9eae9ac4..ec7082984 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -477,7 +477,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp
         (evc,env,lfun,lmatch,goalopt,debug) ast))) cl))
     | Node(_,"TACTIC",[ast]) ->
-      VArg (Tac (tac_interp lfun lmatch debug ast))
+      VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
 (*Remains to treat*)
     | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
       VArg ((Fixexp (id_of_string s,n,c)))
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 481a3a616..4df69a0cd 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -206,8 +206,10 @@ let tclTHENLIST      = tclTHENLIST
 let tclTHEN_i        = tclTHEN_i
 let tclTHENL         = tclTHENL
 let tclTHENS         = tclTHENS
+let tclTHENST        = tclTHENST
 let tclTHENSI        = tclTHENSI
 let tclREPEAT        = tclREPEAT
+let tclREPEAT_MAIN   = tclREPEAT_MAIN
 let tclFIRST         = tclFIRST
 let tclSOLVE         = tclSOLVE
 let tclTRY           = tclTRY
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 717c5212f..ee80beba8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -126,8 +126,10 @@ val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
+val tclTHENST        : tactic -> tactic list -> tactic -> tactic
 val tclTHENSI        : tactic -> tactic list -> tactic
 val tclREPEAT        : tactic -> tactic
+val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic