]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/grafiteAstPp.ml
added a minimal parser to extract informations relevant to dependencies calculation
[helm.git] / helm / ocaml / cic_notation / grafiteAstPp.ml
index 0c63d2594d0ea4e4398a7902981302ee2e7aa47c..6a8e79bc10722535c8dff3df30ab016144ace9fe 100644 (file)
@@ -341,3 +341,8 @@ let pp_cic_command = function
   | Notation _
   | Obj _ -> assert false (* not implemented *)
 
+let pp_dependency = function
+  | IncludeDep str -> "include \"" ^ str ^ "\""
+  | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
+  | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+