Ground Update.

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

2 files changed, 29 insertions, 0 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index dad31af9c..e68b4bf4a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -530,6 +530,28 @@ let rec tclFIRST = function
   | [] -> tclFAIL_s "No applicable tactic."
   |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
+let ite_gen tcal tac_if continue tac_else=
+  let success=ref false in
+  let tac_if0 gl=
+    let result=tac_if gl in
+      success:=true;result in
+  let tac_else0 gl=
+    if !success then 
+      tclFAIL_s "failure in THEN branch" gl 
+    else 
+      tac_else gl in
+    tclORELSE0 (tcal tac_if0 continue)  (tac_else0)  
+    
+(* Try the first tactic and, if it succeeds, continue with 
+   the second one, and if it fails, use the third one *)
+
+let tclIFTHENELSE=ite_gen tclTHEN
+
+(* Idem with tclTHENS and tclTHENSV *)
+
+let tclIFTHENSELSE=ite_gen tclTHENS
+
+let tclIFTHENSVELSE=ite_gen tclTHENSV
 
 
 (* Fails if a tactic did not solve the goal *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 01ffae0d4..2e6f22de1 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,6 +137,13 @@ val tclWEAK_PROGRESS : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 val tclINFO          : tactic -> tactic
 
+(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
+   if it succeeds, applies [tac2] to the resulting subgoals, 
+   and if not applies [tac3] to the initial goal [gls] *)
+val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
+val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
+
 (*s Tactics handling a list of goals. *)
 
 type validation_list = proof_tree list -> proof_tree list