From: Claudio Sacerdoti Coen Date: Thu, 17 May 2012 11:33:34 +0000 (+0000) Subject: Efficient hashing used. X-Git-Tag: make_still_working~1719 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6ab6822e9fa00e8f0ee41421693159a81e47dd5;p=helm.git Efficient hashing used. --- diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index b8a3dd44a..25bc63761 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -26,9 +26,9 @@ let app_counter = ref 0 module RHT = struct type t = NReference.reference - let equal = (==) - let compare = Pervasives.compare - let hash = Hashtbl.hash + let equal = NReference.eq + let compare = NReference.compare + let hash = NReferece.hash end;; module RefHash = Hashtbl.Make(RHT);;