then_ tactical implemented (equivalent to the tclTHEN of Coq)

[helm.git] / helm / gTopLevel / ring.mli

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