]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
Parts of the status were not re-initialized correctly during a reset.
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 840a6e22017147b6a8b92587f235915b6d80edf1..73905eef306be23960b89d239e2ff473f7ce4ff3 100644 (file)
@@ -531,7 +531,7 @@ let record_index_obj =
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
- prerr_endline (string_of_int height);
+ (*prerr_endline (string_of_int height);*)
  let mk_item orig_ty spec =
    let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
    let keys = 
@@ -618,11 +618,11 @@ let index_eq_for_auto status uri =
    let newstatus = index_eq uri status in
      if newstatus == status then status 
      else
-       (prerr_endline ("recording " ^ (NUri.string_of_uri uri));
+       ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
        let dump = record_index_eq uri :: newstatus#dump 
        in newstatus#set_dump dump)
  else 
-   (prerr_endline "Not a fact";
+   ((*prerr_endline "Not a fact";*)
    status)
 ;;