From d284e59636c616c289b9705fb12fa12901e285c3 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 6 Jul 2012 15:58:13 +0000 Subject: Fix order of introduction of hints to preserve most-recent-first semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15538 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 3b86d82621..161fe66fc0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -397,7 +397,7 @@ module Hint_db = struct let db = if db.use_dn && rebuild then rebuild_db st' db else db in addkv k (next_hint_id db) v db - let add_list l db = List.fold_right add_one l db + let add_list l db = List.fold_left (fun db k -> add_one k db) db l let remove_sdl p sdl = list_smartfilter p sdl let remove_he st p (sl1, sl2, dn as he) = -- cgit v1.2.3