]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/getter.mli
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / interface / getter.mli
index c44aa3e435bebfec8e72834887bad64ca6cb825b..0c7401cbc55fffd575ebb525b701546708e585c4 100644 (file)
@@ -33,6 +33,9 @@
 (*                                                                            *)
 (******************************************************************************)
 
+(* raw_get : uri -> dest_file -> () *)
+val raw_get : string -> string -> unit
+
 (* get : uri -> filename *)
 (* If uri is the URI of an annotation, the annotated object is processed *)
 val get : UriManager.uri -> string