diff options
| -rw-r--r-- | library/heads.ml | 13 |
1 files changed, 6 insertions, 7 deletions
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 = |