X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaEngine.mli;fp=matita%2FmatitaEngine.mli;h=bb4537d8db899fb34b71b89983aa7969bbc3c02e;hb=f06968e452cca8782e822d98bec9007404abcbbe;hp=1db991f518c4fab52bd0382b4f8c8ede9869cda0;hpb=94267002fc18aa42a8c09779ad6485f93c3e90fa;p=helm.git

diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli
index 1db991f51..bb4537d8d 100644
--- a/matita/matitaEngine.mli
+++ b/matita/matitaEngine.mli
@@ -39,12 +39,13 @@ val eval_ast :
 (* heavy checks slow down the compilation process but give you some interesting
  * infos like if the theorem is a duplicate *)
 
+exception EnrichedWithLexiconStatus of exn * LexiconEngine.status
+
 (* should be used only by the compiler since it looses the
    * disambiguation_context (text,prefix_len,_) *)
 val eval_from_stream :
   first_statement_only:bool ->
   include_paths:string list ->
-  ?prompt:bool ->
   ?do_heavy_checks:bool ->
   ?enforce_no_new_aliases:bool -> (* default true *)
   ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) ->