big change in parsing, trying to make all functional

[helm.git] / matita / components / grafite / grafiteAst.ml

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e32131a0670afb1819b1b057e197fe0f9e3887a5..46dfef45120af6c1fde10a74653e928972bd65e4 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -84,7 +84,7 @@ type nmacro =
 let magic = 35
 
 type command =
-  | Include of loc * string 
+  | Include of loc * string * unit * string
   | Set of loc * string * string
   | Print of loc * string