]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaEngine.mli
dead code removed
[helm.git] / matita / matita / matitaEngine.mli
index e559d5a0ca4f9f63a18350d8b9959a849df4dd77..6297a57bc7555f3008e5859758d3807c47b4e5a2 100644 (file)
@@ -41,7 +41,6 @@ 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 :
-  first_statement_only:bool ->
   include_paths:string list ->
   ?do_heavy_checks:bool ->
   ?enforce_no_new_aliases:bool -> (* default true *)