]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/grafiteAst.ml
added a minimal parser to extract informations relevant to dependencies calculation
[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml
index 4697ab6adceca84e0d566ffb66374458a6dbc844..f406c44a885d4870333c21b7dfc0e55cef24f803 100644 (file)
@@ -190,3 +190,9 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
   | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
   | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
 
+  (* statements meaningful for matitadep *)
+type dependency =
+  | IncludeDep of string
+  | BaseuriDep of string
+  | UriDep of UriManager.uri
+