big change in parsing, trying to make all functional

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

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index d383448249bf0743bbc172103e3bb917c3b5a42c..202e1776c53436863a2153c5a4ce55fdb90b7863 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -130,7 +130,7 @@ let pp_ncommand = function
 ;;
     
 let pp_command = function
-  | Include (_,path) -> "include \"" ^ path ^ "\""
+  | Include (_,path,_,_) -> "include \"" ^ path ^ "\""
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value