From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 kernel/retroknowledge.ml | 2 +-
 kernel/term.ml           | 3 ++-
 kernel/term.mli          | 5 ++++-
 3 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 970bc0fcc5..ea53d00d7b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -83,7 +83,7 @@ type flags = {fastcomputation : bool}
 (* The [proactive] knowledge contains the mapping [field->entry]. *)
 
 module Proactive =
-  Map.Make (struct type t = field let compare = compare end)
+  Map.Make (struct type t = field let compare = Pervasives.compare end)
 
 type proactive = entry Proactive.t
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 07a85329ef..b90718358e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -143,7 +143,8 @@ let leq_constr_univs = Constr.leq_constr_univs
 let eq_constr_nounivs = Constr.eq_constr_nounivs
 
 let kind_of_term = Constr.kind
-let constr_ord = Constr.compare
+let compare = Constr.compare
+let constr_ord = compare
 let fold_constr = Constr.fold
 let map_puniverses = Constr.map_puniverses
 let map_constr = Constr.map
diff --git a/kernel/term.mli b/kernel/term.mli
index 241ef322fa..e729439f01 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -447,9 +447,12 @@ val eq_constr_nounivs : constr -> constr -> bool
 val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
 (** Alias for [Constr.kind] *)
 
-val constr_ord : constr -> constr -> int
+val compare : constr -> constr -> int
 (** Alias for [Constr.compare] *)
 
+val constr_ord : constr -> constr -> int
+(** Alias for [Term.compare] *)
+
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 (** Alias for [Constr.fold] *)
 
-- 
cgit v1.2.3