Partially restore the suppose tactic

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index f76b8b02a802e80a406e1d9b8321c47b5e2b9087..be7154179812b0df00929c80a47541928f7c7819 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -482,6 +482,7 @@ let eval_ng_tac tac =
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
   |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t
+  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;