diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 14:51:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 14:55:24 +0100 |
| commit | 1995076f64d860d472d882d7d0442f66a07f015c (patch) | |
| tree | ba20e5034328477ee7aa337a92e7ea414dfe3c82 /library/heads.ml | |
| parent | e372b7244bcb8cc449196c29a7dabee6f7f84aa2 (diff) | |
Fixing a Pervasive.compare.
Diffstat (limited to 'library/heads.ml')
| -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 = |