diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /library/globnames.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'library/globnames.ml')
-rw-r--r-- | library/globnames.ml | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 6c9c813e..6383a1f8 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) @@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false let isIndRef = function IndRef _ -> true | _ -> false let isConstructRef = function ConstructRef _ -> true | _ -> false -let eq_gr gr1 gr2 = - gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 - | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 - | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 - | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | _ -> false - let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" @@ -95,8 +87,6 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -let reference_of_constr = global_of_constr - let global_eq_gen eq_cst eq_ind eq_cons x y = x == y || match x, y with @@ -245,3 +235,6 @@ let pop_global_reference = function | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) | VarRef id -> anomaly (Pp.str "VarRef not poppable.") + +(* Deprecated *) +let eq_gr = GlobRef.equal |