Partially restore the suppose tactic

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

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index 532ffbb3767b983780b5e42140677e72a2294c9d..ae07c18ee7361ffad9188ba0171a89fe61804146 100644 (file)
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -28,3 +28,7 @@ open NTactics
 
 let assume name ty =
     exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne)))
+
+let suppose t id t1 =
+    let t1 = match t1 with None -> t | Some t1 -> t1 in
+    exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit `JustOne)))