From b80cf566a39efe65f5ef0b1cc4ff9bb295a67fc7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Mar 2014 14:47:39 +0100
Subject: Fixing generic equality in Auto.

---
 tactics/auto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45f92a97fe..e872baf28e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -401,7 +401,7 @@ module Hint_db = struct
 
   let remove_list grs db =
     let filter (_, h) =
-      match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
+      match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
-- 
cgit v1.2.3