]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_parser/grafiteParser.ml
irediced usage of matita.includes, that is now set by
[helm.git] / components / grafite_parser / grafiteParser.ml
index b5d803f9dcfc0dfce8b36f03782d49c84e9f711f..c948272ef40ff913d6817275fbfdc4d4b10df460 100644 (file)
@@ -692,7 +692,7 @@ EXTEND
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
-       let _root, buri, fullpath = 
+       let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
         in
         let status =
@@ -728,3 +728,4 @@ let exc_located_wrapper f =
 let parse_statement lexbuf =
   exc_located_wrapper
     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+