]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite2/grafiteMisc.mli
New tactic: inversion.
[helm.git] / helm / ocaml / grafite2 / grafiteMisc.mli
index 8cc384abcd0d38abf3d40691d024cda17f9ae823..833bb6360de768d0c05f35f19cac7c2209d9dd31 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-val baseuri_of_baseuri_decl :
- ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
-  string option
-
   (** check whether no objects are defined below a given baseuri *)
 val is_empty: string -> bool
-
-val baseuri_of_file : string -> string
-
-val obj_file_of_script : basedir:string -> string -> string