diff options
Diffstat (limited to 'library/globnames.ml')
| -rw-r--r-- | library/globnames.ml | 50 |
1 files changed, 26 insertions, 24 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index a78f5f13..6c9c813e 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,21 +1,23 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors open Names -open Term +open Constr open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = +type global_reference = Names.global_reference = | VarRef of variable (** A reference to the section-context. *) - | ConstRef of constant (** A reference to the environment. *) + | ConstRef of Constant.t (** 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. *) @@ -26,7 +28,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false let eq_gr gr1 gr2 = gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 + | 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 @@ -67,12 +69,12 @@ let subst_global subst ref = match ref with if c'==c then ref,t else ConstructRef c', t let canonical_gr = function - | ConstRef con -> ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con)) + | IndRef (kn,i) -> IndRef(MutInd.make1(MutInd.canonical kn),i) + | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j) | VarRef id -> VarRef id -let global_of_constr c = match kind_of_term c with +let global_of_constr c = match kind c with | Const (sp,u) -> ConstRef sp | Ind (ind_sp,u) -> IndRef ind_sp | Construct (cstr_cp,u) -> ConstructRef cstr_cp @@ -80,11 +82,11 @@ let global_of_constr c = match kind_of_term c with | _ -> raise Not_found let is_global c t = - match c, kind_of_term t with - | ConstRef c, Const (c', _) -> eq_constant c c' + match c, kind t with + | ConstRef c, Const (c', _) -> Constant.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> id_eq id id' + | VarRef id, Var id' -> Id.equal id id' | _ -> false let printable_constr_of_global = function @@ -157,7 +159,7 @@ module Refset_env = Refmap_env.Set (* Extended global references *) -type syndef_name = kernel_name +type syndef_name = KerName.t type extended_global_reference = | TrueGlobal of global_reference @@ -180,7 +182,7 @@ module ExtRefOrdered = struct if x == y then 0 else match x, y with | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry - | SynDef knx, SynDef kny -> kn_ord knx kny + | SynDef knx, SynDef kny -> KerName.compare knx kny | TrueGlobal _, SynDef _ -> -1 | SynDef _, TrueGlobal _ -> 1 @@ -215,12 +217,12 @@ let decode_mind kn = id::(DirPath.repr dp) | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp) in - let mp,sec_dir,l = repr_mind kn in + let mp,sec_dir,l = MutInd.repr3 kn in check_empty_section sec_dir; (DirPath.make (dir_of_mp mp)),Label.to_id l let decode_con kn = - let mp,sec_dir,l = repr_con kn in + let mp,sec_dir,l = Constant.repr3 kn in check_empty_section sec_dir; match mp with | MPfile dir -> (dir,Label.to_id l) @@ -231,15 +233,15 @@ let decode_con kn = user and canonical kernel names must be equal. *) let pop_con con = - let (mp,dir,l) = repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l let pop_kn kn = - let (mp,dir,l) = repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_global_reference = function | ConstRef con -> ConstRef (pop_con con) | 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") + | VarRef id -> anomaly (Pp.str "VarRef not poppable.") |