diff options
Diffstat (limited to 'library/globnames.ml')
| -rw-r--r-- | library/globnames.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 829e2cefc..bec463ecf 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -115,7 +115,7 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = | _, ConstRef _ -> 1 | IndRef indx, IndRef indy -> ord_ind indx indy | IndRef _, _ -> -1 - | _ , IndRef _ -> -1 + | _ , IndRef _ -> 1 | ConstructRef consx, ConstructRef consy -> ord_cons consx consy let global_hash_gen hash_cst hash_ind hash_cons gr = |