Removing some generic equalities.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index e80197030..af4ebde7f 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -82,7 +82,13 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = match x, y with
   | IndRef indx, IndRef indy -> ord_ind indx indy
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
   | VarRef v1, VarRef v2 -> Id.compare v1 v2
-  | _, _ -> Pervasives.compare x y
+
+  | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1
+  | ConstRef _, VarRef _ -> 1
+  | ConstRef _, (IndRef _ | ConstructRef _) -> -1
+  | IndRef _, (VarRef _ | ConstRef _) -> 1
+  | IndRef _, ConstructRef _ -> -1
+  | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
 
 let global_ord_can =
   global_ord_gen con_ord ind_ord constructor_ord