- cleanup

[helm.git] / matita / matita / matitaEngine.mli

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 9332d97223e06fa6d635ae9d999cd4ceac156021..29f3a5a0b64169649655dfb29c1738b19d3b7aec 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -41,11 +41,16 @@ exception EnrichedWithStatus of exn * GrafiteTypes.status
 (* should be used only by the compiler since it looses the
    * disambiguation_context (text,prefix_len,_) *)
 val eval_from_stream :
-  include_paths:string list ->
-  ?do_heavy_checks:bool ->
-  ?enforce_no_new_aliases:bool -> (* default true *)
-  GrafiteTypes.status ->
-  Ulexing.lexbuf ->
-  (GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
-  (GrafiteTypes.status *
-   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
+  include_paths:string list -> ?do_heavy_checks:bool -> GrafiteTypes.status ->
+   Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
+    GrafiteTypes.status
+
+val toplevel:
+  #GrafiteParser.status -> include_paths:string list -> string ->
+    GrafiteParser.ast_statement
+
+(* EX MATITACLIB *)
+module Make : sig
+   val make: string -> string list -> bool
+end
+(* FINE EX MATITACLIB *)