1. Several files in grafite that should be in grafite_parser moved there.

[helm.git] / helm / ocaml / grafite2 / grafiteEngine.mli

diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite2/grafiteEngine.mli
index efebbf0486da4abfae34e7ab4d8fc69228d7b656..e317060b580e2c84a544dbbcd88c0e298526d393 100644 (file)
--- a/helm/ocaml/grafite2/grafiteEngine.mli
+++ b/helm/ocaml/grafite2/grafiteEngine.mli
@@ -24,10 +24,11 @@
  *)
 
 exception Drop
-exception UnableToInclude of string
 exception IncludedFileNotCompiled of string
 
 val eval_ast :
+  baseuri_of_script:(string -> string) ->
+
   disambiguate_tactic:
    (GrafiteTypes.status ->
     ProofEngineTypes.goal ->
@@ -41,7 +42,6 @@ val eval_ast :
     GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
 
   ?do_heavy_checks:bool ->
-  ?include_paths:string list ->
   ?clean_baseuri:bool ->
   GrafiteTypes.status ->
   ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->