diff options
author | 2013-08-03 20:45:46 +0000 | |
---|---|---|
committer | 2013-08-03 20:45:46 +0000 | |
commit | 40c29ed04ee15c34ef34f7ba638a0773dd113f92 (patch) | |
tree | 2911881711d18316699a1b5d74edb66489088d56 /tactics | |
parent | 2b8ad61822111fad93176b54800cb43e347df292 (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.ml | 5 |
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 *) |