From e6ab6822e9fa00e8f0ee41421693159a81e47dd5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 May 2012 11:33:34 +0000 Subject: [PATCH] Efficient hashing used. --- matita/components/ng_tactics/nnAuto.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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);; -- 2.39.2