diff options
| author | msozeau | 2012-07-06 15:58:13 +0000 |
|---|---|---|
| committer | msozeau | 2012-07-06 15:58:13 +0000 |
| commit | d284e59636c616c289b9705fb12fa12901e285c3 (patch) | |
| tree | 102713bb1ab0a83de1e56b1d9d3195ad78378aaa | |
| parent | 2bf066d9ffcacd7a78d4bc278f7a7909ce4f9a79 (diff) | |
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
| -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 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) = |