From 89e59b9a578fa761ebc12e3a8e01c3b838301266 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Mar 2014 16:10:51 +0100 Subject: Tentative fix for a very strange pervasive equality in Auto. --- tactics/auto.ml | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) 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 -> -- cgit v1.2.3