From c36b71880e58e39de8444efdd2a3c68047af9eda Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 13 Sep 2002 11:10:30 +0000
Subject: [PATCH] then_ tactical implemented (equivalent to the tclTHEN of Coq)

---
 helm/gTopLevel/ring.ml  | 9 +++++++++
 helm/gTopLevel/ring.mli | 3 +++
 2 files changed, 12 insertions(+)

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
-- 
2.39.2