From 1995076f64d860d472d882d7d0442f66a07f015c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Feb 2014 14:51:07 +0100 Subject: Fixing a Pervasive.compare. --- library/heads.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'library/heads.ml') diff --git a/library/heads.ml b/library/heads.ml index c52a5eb23..f64cdb05a 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -40,13 +40,12 @@ type head_approximation = module Evalreford = struct type t = evaluable_global_reference - let compare x y = - let make_name = function - | EvalConstRef con -> - EvalConstRef(constant_of_kn(canonical_con con)) - | k -> k - in - Pervasives.compare (make_name x) (make_name y) + let compare gr1 gr2 = match gr1, gr2 with + | EvalVarRef id1, EvalVarRef id2 -> Id.compare id1 id2 + | EvalVarRef _, EvalConstRef _ -> -1 + | EvalConstRef c1, EvalConstRef c2 -> + Constant.CanOrd.compare c1 c2 + | EvalConstRef _, EvalVarRef _ -> 1 end module Evalrefmap = -- cgit v1.2.3