Partially restore the suppose tactic

[helm.git] / matita / components / ng_tactics / declarative.mli

diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli
index f6f0ff953f8753d2c24f28c64c93550beedb7588..a7ec0e44d12260c8ba840e831e6e6991ef120c25 100644 (file)
--- a/matita/components/ng_tactics/declarative.mli
+++ b/matita/components/ng_tactics/declarative.mli
@@ -24,3 +24,4 @@
  *)
 
 val assume : string -> NotationPt.term -> 's NTacStatus.tactic
+val suppose : NotationPt.term -> string -> NotationPt.term option -> 's NTacStatus.tactic