PrimitiveTactics: intros _ now aveilable

[helm.git] / components / tptp_grafite / tptp2grafite.ml

diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml
index 3ed457d958dd64d25ee7d29ab111ad53574563c2..fa280b3f8adcd864496eb94af4440d1a445aa324 100644 (file)
--- a/components/tptp_grafite/tptp2grafite.ml
+++ b/components/tptp_grafite/tptp2grafite.ml
@@ -247,7 +247,7 @@ let convert_ast statements context = function
           statements @ [
             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
             GA.Executable(floc,GA.Tactic(floc, Some
-             (GA.Intros (floc,None,[])),GA.Dot(floc)))] @
+             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
           (if fv <> [] then     
             (List.flatten
               (List.map