aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-03 20:45:46 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-03 20:45:46 +0000
commit40c29ed04ee15c34ef34f7ba638a0773dd113f92 (patch)
tree2911881711d18316699a1b5d74edb66489088d56 /tactics
parent2b8ad61822111fad93176b54800cb43e347df292 (diff)
Small fixes due to the arrival of OCaml 3.12.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16656 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 39d9fe766..fab324962 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -463,10 +463,7 @@ let searchtable_add (name,db) =
let current_db_names () =
let fold k _ acc = k :: acc in
List.rev (Hintdbmap.fold fold !searchtable [])
-(** FIXME: from 3.12 use Map.keys *)
-let current_db () =
- let fold k v acc = (k, v) :: acc in
- List.rev (Hintdbmap.fold fold !searchtable [])
+let current_db () = Hintdbmap.bindings !searchtable
(**************************************************************************)
(* Definition of the summary *)