then_ tactical implemented (equivalent to the tclTHEN of Coq)

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 0b5cfadd27acbf686ecbb71ce1620d62d32de5f8..69f4b87a3939c609e82bacebbe5d0914703861a6 100644 (file)
--- 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 66ad9b121235554d4d664da22753b2e862d37242..67bc1a164ec2dc64e8c50892db31daa2584a0e2a 100644 (file)
--- 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