X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;fp=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;h=ae07c18ee7361ffad9188ba0171a89fe61804146;hb=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42;hp=532ffbb3767b983780b5e42140677e72a2294c9d;hpb=b6ceb877c05d27705ef163488aee38e60a86886c;p=helm.git

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index 532ffbb37..ae07c18ee 100644
--- 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)))