From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 13 Sep 2002 11:10:30 +0000 (+0000)
Subject: then_ tactical implemented (equivalent to the tclTHEN of Coq)
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~78
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c36b71880e58e39de8444efdd2a3c68047af9eda;p=helm.git

then_ tactical implemented (equivalent to the tclTHEN of Coq)
---

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 0b5cfadd2..69f4b87a3 100644
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -411,6 +411,15 @@ let thens ~start ~continuations ~status =
   with
    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
 
+let then_ ~start ~continuation ~status =
+ let (proof,new_goals) = start ~status in
+  List.fold_left
+   (fun (proof,goals) goal ->
+     let (proof',new_goals') = continuation ~status:(proof,goal) in
+      (proof',goals@new_goals')
+   ) (proof,[]) new_goals
+
+
 let id_tac ~status:(proof,goal) =
  (proof,[goal])
 
diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli
index 66ad9b121..67bc1a164 100644
--- a/helm/gTopLevel/ring.mli
+++ b/helm/gTopLevel/ring.mli
@@ -13,3 +13,6 @@ val try_tactics:
 val thens:
  start: ProofEngineTypes.tactic ->
  continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+val then_:
+ start: ProofEngineTypes.tactic ->
+ continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic