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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 |
2 files changed, 2 insertions, 4 deletions
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 |