dead code removed

[helm.git] / matita / matita / matitaEngine.ml

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 =