From: Andrea Asperti Date: Mon, 8 Feb 2010 07:26:18 +0000 (+0000) Subject: Bug fixing. X-Git-Tag: make_still_working~3049 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de94ff76a34259735fd1aca76504c2676773cb73;p=helm.git Bug fixing. --- diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 73905eef3..73118fa56 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -616,7 +616,7 @@ let record_index_eq = let index_eq_for_auto status uri = if NnAuto.is_a_fact_obj status uri then let newstatus = index_eq uri status in - if newstatus == status then status + if newstatus#eq_cache == status#eq_cache then status else ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*) let dump = record_index_eq uri :: newstatus#dump