snopshot (working one!)

[helm.git] / matita / matitaEngine.mli

diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli
index 1db991f518c4fab52bd0382b4f8c8ede9869cda0..bb4537d8db899fb34b71b89983aa7969bbc3c02e 100644 (file)
--- 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) ->