update in basic_2

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

diff --git a/matitaB/matita/matitaEngine.mli b/matitaB/matita/matitaEngine.mli
index d412d3ad03b1555a49cfe0c565bb80789eea25f5..ea19ef41df3bbfc42c560f9e54c9c3111b211bba 100644 (file)
--- a/matitaB/matita/matitaEngine.mli
+++ b/matitaB/matita/matitaEngine.mli
@@ -30,7 +30,7 @@ exception FailureCompiling of string * exn
 exception CircularDependency of string
 
 class status:
- string ->
+ string option -> string ->
   object
    inherit GrafiteTypes.status
    inherit ApplyTransformation.status
@@ -48,7 +48,8 @@ val eval_ast :
   GrafiteTypes.status ->
   string * int *
   GrafiteAst.statement ->
-  (GrafiteTypes.status *
-   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
+  GrafiteTypes.status 
 
-val assert_ng: include_paths:string list -> string -> bool
+val assert_ng: include_paths:string list -> ?outch:out_channel -> string -> bool
+
+val eos : GrafiteTypes.status -> string -> bool