diff options
| author | ppedrot | 2013-08-03 20:45:46 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-03 20:45:46 +0000 |
| commit | 40c29ed04ee15c34ef34f7ba638a0773dd113f92 (patch) | |
| tree | 2911881711d18316699a1b5d74edb66489088d56 | |
| 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
| -rw-r--r-- | kernel/names.mli | 7 | ||||
| -rw-r--r-- | pretyping/classops.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | tactics/auto.ml | 5 |
4 files changed, 4 insertions, 14 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index c2409649c0..8022cb199e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -35,12 +35,7 @@ sig module Set : Set.S with type elt = t (** Finite sets of identifiers. *) - module Map : sig - include Map.S with type key = t - (** FIXME: this is included in OCaml 3.12 *) - val exists : (key -> 'a -> bool) -> 'a t -> bool - val singleton : key -> 'a -> 'a t - end + module Map : Map.S with type key = t (** Finite maps of identifiers. *) module Pred : Predicate.S with type elt = t diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 3333845057..1e1f2184c4 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -479,9 +479,7 @@ let coercions () = List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) let inheritance_graph () = - (** FIXME: in 3.12 use Map.keys *) - let fold k v acc = (k, v) :: acc in - ClPairMap.fold fold !inheritance_graph [] + ClPairMap.bindings !inheritance_graph let coercion_of_reference r = let ref = Nametab.global r in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6f56f1bfa3..932b4cdc1e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -520,7 +520,7 @@ let univ_of_sort = function | Prop Null -> Univ.type0m_univ let is_eq_sort s1 s2 = - if Int.equal (sorts_ord s1 s2) 0 then None (* FIXME *) + if Sorts.equal s1 s2 then None else let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in diff --git a/tactics/auto.ml b/tactics/auto.ml index 39d9fe766e..fab324962b 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 *) |