From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 library/globnames.ml | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'library/globnames.ml')

diff --git a/library/globnames.ml b/library/globnames.ml
index 3ae44b2c..a78f5f13 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Names
 open Term
 open Mod_subst
@@ -14,10 +14,10 @@ open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
 type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
+  | VarRef of variable           (** A reference to the section-context. *)
+  | ConstRef of constant         (** A reference to the environment. *)
+  | IndRef of inductive          (** A reference to an inductive type. *)
+  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
 
 let isVarRef = function VarRef _ -> true | _ -> false
 let isConstRef = function ConstRef _ -> true | _ -> false
@@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y =
 let global_ord_gen ord_cst ord_ind ord_cons x y =
   if x == y then 0
   else match x, y with
+  | VarRef v1, VarRef v2 -> Id.compare v1 v2
+  | VarRef _, _ -> -1
+  | _, VarRef _ -> 1
   | ConstRef cx, ConstRef cy -> ord_cst cx cy
+  | ConstRef _, _ -> -1
+  | _, ConstRef _ -> 1
   | IndRef indx, IndRef indy -> ord_ind indx indy
+  | IndRef _, _ -> -1
+  | _ , IndRef _ -> 1
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-  | VarRef v1, VarRef v2 -> Id.compare v1 v2
-
-  | 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_hash_gen hash_cst hash_ind hash_cons gr =
   let open Hashset.Combine in
-- 
cgit v1.2.3