Tentative fix for a very strange pervasive equality in Auto.

1 files changed, 24 insertions, 1 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e872baf28..632f83c83 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,6 +72,27 @@ type pri_auto_tactic = clausenv gen_auto_tactic
 
 type hint_entry = global_reference option * types gen_auto_tactic
 
+let eq_hints_path_atom p1 p2 = match p1, p2 with
+| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
+| PathAny, PathAny -> true
+| (PathHints _ | PathAny), _ -> false
+
+let eq_auto_tactic t1 t2 = match t1, t2 with
+| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2
+| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2
+| Give_exact c1, Give_exact c2 -> Constr.equal c1 c2
+| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2
+| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2
+| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *)
+| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
+  | Unfold_nth _ | Extern _), _ -> false
+
+let eq_gen_auto_tactic t1 t2 =
+  Int.equal t1.pri t2.pri &&
+  Option.equal constr_pattern_eq t1.pat t2.pat &&
+  eq_hints_path_atom t1.name t2.name &&
+  eq_auto_tactic t1.code t2.code
+
 let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
   let d = pri1 - pri2 in
     if Int.equal d 0 then id2 - id1
@@ -360,7 +381,9 @@ module Hint_db = struct
     let pat = if not db.use_dn && is_exact v.code then None else v.pat in
       match k with
       | None ->
-	  if not (List.exists (fun (_, (_, v')) -> Pervasives.(=) v v') db.hintdb_nopat) then (** FIXME *)
+          (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
+          let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
+	  if not (List.exists is_present db.hintdb_nopat) then
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
 	  else db
       | Some gr ->