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/term.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 07a85329e..b90718358 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 -- cgit v1.2.3