From 4dd61c9459a7388078bbd2e1b6f07959c4c72001 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 16 Oct 2015 07:45:19 +0200
Subject: Merge hint lists instead of appending them. (Fix bug #3199)

---
 tactics/hints.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 96c7d79ca5..2755ed9cb0 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -458,7 +458,9 @@ module Hint_db = struct
     else List.exists (matches_mode args) modes
 
   let merge_entry db nopat pat =
-    let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+    let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
+    let h = List.merge pri_order_int h nopat in
+    let h = List.merge pri_order_int h pat in
     List.map realize_tac h
 
   let map_none db =
@@ -562,7 +564,9 @@ module Hint_db = struct
 
   let remove_one gr db = remove_list [gr] db
 
-  let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+  let get_entry se =
+    let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
+    List.map realize_tac h
 
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
-- 
cgit v1.2.3