dead code removed

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 429f75cd371806755c0cafd1bdf00044bdfbf7fa..aa854e2dfeaacfbd153968fffd9443f48498cc98 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -86,16 +86,11 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
 exception TryingToAdd of string
 exception EnrichedWithStatus of exn * GrafiteTypes.status
 
-let eval_from_stream ~first_statement_only ~include_paths 
- ?do_heavy_checks ?(enforce_no_new_aliases=true)
- ?(watch_statuses=fun _ -> ()) status str cb 
+let eval_from_stream ~include_paths ?do_heavy_checks
+ ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ -> ()) status str cb 
 =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
  let rec loop status statuses =
-  let loop =
-   if first_statement_only then fun _ statuses -> statuses
-   else loop
-  in
   let stop,g,s = 
    try
      let cont =

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index e559d5a0ca4f9f63a18350d8b9959a849df4dd77..6297a57bc7555f3008e5859758d3807c47b4e5a2 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -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 *)

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index d1962c99d74c6beea27c41990009c3324529546c..b4168ba94ca47fba77bafe84f011cbc9d998bcc2 100644 (file)
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -166,8 +166,7 @@ let compile atstart options fname =
     let grafite_status =
      let rec aux_for_dump x grafite_status =
       match
-       MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
-        grafite_status buf x
+       MatitaEngine.eval_from_stream ~include_paths grafite_status buf x
       with
       | [] -> grafite_status
       | (g,None)::_ -> g