diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-07 14:47:39 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-07 14:49:00 +0100 |
commit | b80cf566a39efe65f5ef0b1cc4ff9bb295a67fc7 (patch) | |
tree | 94a62b58716db8409a6f8e6bb7ad188b317bd47b | |
parent | 588c472b926c674066f17f1a221593e1329b6067 (diff) |
Fixing generic equality in Auto.
-rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 45f92a97f..e872baf28 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 } |