diff options
164 files changed, 483 insertions, 406 deletions
diff --git a/dev/base_include b/dev/base_include index a0c4928f6..1e692defb 100644 --- a/dev/base_include +++ b/dev/base_include @@ -64,6 +64,7 @@ open Declare open Declaremods open Impargs open Libnames +open Globnames open Nametab open Library diff --git a/dev/printers.mllib b/dev/printers.mllib index 955eb3650..545a1881f 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -60,6 +60,7 @@ Safe_typing Summary Nameops Libnames +Globnames Global Nametab Libobject diff --git a/dev/top_printers.ml b/dev/top_printers.ml index c765f3848..4fd6171ac 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -14,6 +14,7 @@ open Util open Pp open Names open Libnames +open Globnames open Nameops open Sign open Univ diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 87a5ce73b..38fe7a1ca 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -20,6 +20,7 @@ open Inductive open Sign open Environ open Libnames +open Globnames open Impargs open Constrexpr open Constrexpr_ops diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 38f8b6579..0c5d4b589 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -13,6 +13,7 @@ open Termops open Sign open Environ open Libnames +open Globnames open Nametab open Glob_term open Pattern diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 480dc6ce2..5a8dcac08 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,6 +14,7 @@ open Names open Nameops open Namegen open Libnames +open Globnames open Impargs open Glob_term open Glob_ops diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 10fbde605..7c682ec42 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -12,6 +12,7 @@ open Sign open Evd open Environ open Libnames +open Globnames open Glob_term open Pattern open Constrexpr diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 9eda0b96a..6f01bb466 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -12,6 +12,7 @@ open Pp open Names open Term open Libnames +open Globnames open Pattern open Nametab open Smartlocate @@ -125,8 +126,8 @@ let jmeq_module_name = ["Coq";"Logic";"JMeq"] let jmeq_module = make_dir jmeq_module_name (* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_mind dir id -let make_con dir id = Libnames.encode_con dir id +let make_kn dir id = Globnames.encode_mind dir id +let make_con dir id = Globnames.encode_con dir id (** Identity *) diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 27137e81b..a77b1060c 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -8,6 +8,7 @@ open Names open Libnames +open Globnames open Nametab open Term open Pattern diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 5ea9cb986..58577356b 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -102,18 +102,18 @@ let type_of_global_ref gr = "class" else match gr with - | Libnames.ConstRef cst -> + | Globnames.ConstRef cst -> type_of_logical_kind (Decls.constant_kind cst) - | Libnames.VarRef v -> + | Globnames.VarRef v -> "var" ^ type_of_logical_kind (Decls.variable_kind v) - | Libnames.IndRef ind -> + | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record then if mib.Declarations.mind_finite then "rec" else "corec" else if mib.Declarations.mind_finite then "ind" else "coind" - | Libnames.ConstructRef _ -> "constr" + | Globnames.ConstructRef _ -> "constr" let remove_sections dir = if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 59a695ee6..16fa04ef9 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -26,7 +26,7 @@ type coqdoc_state = Lexer.location_table val coqdoc_freeze : unit -> coqdoc_state val coqdoc_unfreeze : coqdoc_state -> unit -val add_glob : Pp.loc -> Libnames.global_reference -> unit +val add_glob : Pp.loc -> Globnames.global_reference -> unit val add_glob_kn : Pp.loc -> Names.kernel_name -> unit val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit diff --git a/interp/genarg.mli b/interp/genarg.mli index 3986d135a..2bd19632e 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -10,6 +10,7 @@ open Pp open Names open Term open Libnames +open Globnames open Glob_term open Genredexpr open Pattern diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index d6e7485dc..90b495982 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -20,6 +20,7 @@ open Util open Glob_term open Constrexpr open Libnames +open Globnames open Typeclasses open Typeclasses_errors open Pp diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 3d869a019..6297a17d2 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -18,6 +18,7 @@ open Glob_term open Constrexpr open Pp open Libnames +open Globnames open Typeclasses val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit diff --git a/interp/notation.ml b/interp/notation.ml index f2dec3bc1..64911675b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -15,6 +15,7 @@ open Names open Term open Nametab open Libnames +open Globnames open Summary open Constrexpr open Notation_term diff --git a/interp/notation.mli b/interp/notation.mli index d38f3d6bf..668d827f5 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -13,6 +13,7 @@ open Bigint open Names open Nametab open Libnames +open Globnames open Constrexpr open Glob_term open Notation_term diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f0a20d648..853c6967c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -11,7 +11,7 @@ open Errors open Util open Names open Nameops -open Libnames +open Globnames open Misctypes open Glob_term open Glob_ops diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 176c2a76b..06a73723b 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -6,12 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i*) open Pp -open Errors -open Util open Names -(*i*) (*s Pretty-print. *) diff --git a/interp/reserve.ml b/interp/reserve.ml index 296fb2811..f170ff023 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -17,7 +17,7 @@ open Summary open Libobject open Lib open Notation_term -open Libnames +open Globnames type key = | RefKey of global_reference diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 6146bc42e..0c39c5d47 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -17,6 +17,7 @@ open Errors open Util open Names open Libnames +open Globnames open Misctypes open Syntax_def open Notation_term diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index b4e121b4b..eaa4863c6 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -9,6 +9,7 @@ open Pp open Names open Libnames +open Globnames open Misctypes (** [locate_global_with_alias] locates global reference possibly following diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index fae83ee95..a95e4f2c5 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames (** The kinds of existential variable *) diff --git a/intf/glob_term.mli b/intf/glob_term.mli index d89b5840d..7ee0320f0 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -19,6 +19,7 @@ open Names open Sign open Term open Libnames +open Globnames open Decl_kinds open Misctypes diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 2485fd7a6..c8acc0496 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -8,7 +8,7 @@ open Names open Term -open Libnames +open Globnames open Misctypes open Glob_term diff --git a/intf/pattern.mli b/intf/pattern.mli index 63d4ffa7a..96f6ac9f6 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Term open Misctypes diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e70fc1308..895eca2d9 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -9,6 +9,7 @@ open Names open Constrexpr open Libnames +open Globnames open Nametab open Genredexpr open Genarg diff --git a/library/declare.ml b/library/declare.ml index 10e8f3a5d..c386ac6aa 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -13,6 +13,7 @@ open Errors open Util open Names open Libnames +open Globnames open Nameops open Term open Sign diff --git a/library/global.ml b/library/global.ml index e57aea6c9..cb57248b5 100644 --- a/library/global.ml +++ b/library/global.ml @@ -156,7 +156,7 @@ let import cenv digest = let env_of_context hyps = reset_with_named_context hyps (env()) -open Libnames +open Globnames let type_of_reference env = function | VarRef id -> Environ.named_type id env diff --git a/library/global.mli b/library/global.mli index 77fd465c8..bd7610ed9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -98,7 +98,7 @@ val import : compiled_library -> Digest.t -> module_path (** Function to get an environment from the constants part of the global * environment and a given context. *) -val type_of_global : Libnames.global_reference -> types +val type_of_global : Globnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env diff --git a/library/globnames.ml b/library/globnames.ml new file mode 100644 index 000000000..ae507de25 --- /dev/null +++ b/library/globnames.ml @@ -0,0 +1,174 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Names +open Nameops +open Term +open Mod_subst +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 + +let isVarRef = function VarRef _ -> true | _ -> false +let isConstRef = function ConstRef _ -> true | _ -> false +let isIndRef = function IndRef _ -> true | _ -> false +let isConstructRef = function ConstructRef _ -> true | _ -> false + +let eq_gr gr1 gr2 = + match gr1,gr2 with + | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 + | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2 + | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2 + | _,_ -> gr1=gr2 + +let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" +let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" +let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" +let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" + +let subst_constructor subst ((kn,i),j as ref) = + let kn' = subst_ind subst kn in + if kn==kn' then ref, mkConstruct ref + else ((kn',i),j), mkConstruct ((kn',i),j) + +let subst_global subst ref = match ref with + | VarRef var -> ref, mkVar var + | ConstRef kn -> + let kn',t = subst_con subst kn in + if kn==kn' then ref, mkConst kn else ConstRef kn', t + | IndRef (kn,i) -> + let kn' = subst_ind subst kn in + if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i) + | ConstructRef ((kn,i),j as c) -> + let c',t = subst_constructor subst c in + 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) + | VarRef id -> VarRef id + +let global_of_constr c = match kind_of_term c with + | Const sp -> ConstRef sp + | Ind ind_sp -> IndRef ind_sp + | Construct cstr_cp -> ConstructRef cstr_cp + | Var id -> VarRef id + | _ -> raise Not_found + +let constr_of_global = function + | VarRef id -> mkVar id + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkConstruct sp + | IndRef sp -> mkInd sp + +let constr_of_reference = constr_of_global +let reference_of_constr = global_of_constr + +let global_ord_gen fc fmi x y = + let ind_ord (indx,ix) (indy,iy) = + let c = Pervasives.compare ix iy in + if c = 0 then kn_ord (fmi indx) (fmi indy) else c + in + match x, y with + | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy) + | IndRef indx, IndRef indy -> ind_ord indx indy + | ConstructRef (indx,jx), ConstructRef (indy,jy) -> + let c = Pervasives.compare jx jy in + if c = 0 then ind_ord indx indy else c + | _, _ -> Pervasives.compare x y + +let global_ord_can = global_ord_gen canonical_con canonical_mind +let global_ord_user = global_ord_gen user_con user_mind + +(* By default, [global_reference] are ordered on their canonical part *) + +module RefOrdered = struct + type t = global_reference + let compare = global_ord_can +end + +module RefOrdered_env = struct + type t = global_reference + let compare = global_ord_user +end + +module Refset = Set.Make(RefOrdered) +module Refmap = Map.Make(RefOrdered) + +(* Extended global references *) + +type syndef_name = kernel_name + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + +(* We order [extended_global_reference] via their user part + (cf. pretty printer) *) + +module ExtRefOrdered = struct + type t = extended_global_reference + let compare x y = + match x, y with + | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry + | SynDef knx, SynDef kny -> kn_ord knx kny + | _, _ -> Pervasives.compare x y +end + +(** {6 Temporary function to brutally form kernel names from section paths } *) + +let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id) + +let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) + +let decode_mind kn = + let rec dir_of_mp = function + | MPfile dir -> repr_dirpath dir + | MPbound mbid -> + let _,_,dp = repr_mbid mbid in + let id = id_of_mbid mbid in + id::(repr_dirpath dp) + | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp) + in + let mp,sec_dir,l = repr_mind kn in + if (repr_dirpath sec_dir) = [] then + (make_dirpath (dir_of_mp mp)),id_of_label l + else + anomaly "Section part should be empty!" + +let decode_con kn = + let mp,sec_dir,l = repr_con kn in + match mp,(repr_dirpath sec_dir) with + MPfile dir,[] -> (dir,id_of_label l) + | _ , [] -> anomaly "MPfile expected!" + | _ -> anomaly "Section part should be empty!" + +(* popping one level of section in global names *) + +let pop_con con = + let (mp,dir,l) = repr_con con in + Names.make_con 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 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 "VarRef not poppable" diff --git a/library/globnames.mli b/library/globnames.mli new file mode 100644 index 000000000..b41d04970 --- /dev/null +++ b/library/globnames.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Names +open Term +open Mod_subst + +(** {6 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 + +val isVarRef : global_reference -> bool +val isConstRef : global_reference -> bool +val isIndRef : global_reference -> bool +val isConstructRef : global_reference -> bool + +val eq_gr : global_reference -> global_reference -> bool +val canonical_gr : global_reference -> global_reference + +val destVarRef : global_reference -> variable +val destConstRef : global_reference -> constant +val destIndRef : global_reference -> inductive +val destConstructRef : global_reference -> constructor + + +val subst_constructor : substitution -> constructor -> constructor * constr +val subst_global : substitution -> global_reference -> global_reference * constr + +(** Turn a global reference into a construction *) +val constr_of_global : global_reference -> constr + +(** Turn a construction denoting a global reference into a global reference; + raise [Not_found] if not a global reference *) +val global_of_constr : constr -> global_reference + +(** Obsolete synonyms for constr_of_global and global_of_constr *) +val constr_of_reference : global_reference -> constr +val reference_of_constr : constr -> global_reference + +module RefOrdered : sig + type t = global_reference + val compare : global_reference -> global_reference -> int +end + +module RefOrdered_env : sig + type t = global_reference + val compare : global_reference -> global_reference -> int +end + +module Refset : Set.S with type elt = global_reference +module Refmap : Map.S with type key = global_reference + +(** {6 Extended global references } *) + +type syndef_name = kernel_name + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + +module ExtRefOrdered : sig + type t = extended_global_reference + val compare : t -> t -> int +end + +(** {6 Temporary function to brutally form kernel names from section paths } *) + +val encode_mind : dir_path -> identifier -> mutual_inductive +val decode_mind : mutual_inductive -> dir_path * identifier +val encode_con : dir_path -> identifier -> constant +val decode_con : constant -> dir_path * identifier + +(** {6 Popping one level of section in global names } *) + +val pop_con : constant -> constant +val pop_kn : mutual_inductive-> mutual_inductive +val pop_global_reference : global_reference -> global_reference diff --git a/library/heads.ml b/library/heads.ml index 327b883ee..9ff678fb6 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -14,6 +14,7 @@ open Term open Mod_subst open Environ open Libnames +open Globnames open Nameops open Libobject open Lib diff --git a/library/impargs.ml b/library/impargs.ml index 707b2f4cb..8e9365920 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -9,7 +9,7 @@ open Errors open Util open Names -open Libnames +open Globnames open Term open Reduction open Declarations diff --git a/library/impargs.mli b/library/impargs.mli index 57f1ac71e..0443a6f25 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Term open Environ open Nametab diff --git a/library/lib.ml b/library/lib.ml index ff7e9b841..4e2b7437e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -10,6 +10,7 @@ open Pp open Errors open Util open Libnames +open Globnames open Nameops open Libobject open Summary diff --git a/library/lib.mli b/library/lib.mli index 360eada85..318997067 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -132,8 +132,8 @@ val library_dp : unit -> Names.dir_path val dp_of_mp : Names.module_path -> Names.dir_path val split_mp : Names.module_path -> Names.dir_path * Names.dir_path val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list -val library_part : Libnames.global_reference -> Names.dir_path -val remove_section_part : Libnames.global_reference -> Names.dir_path +val library_part : Globnames.global_reference -> Names.dir_path +val remove_section_part : Globnames.global_reference -> Names.dir_path (** {6 Sections } *) @@ -187,8 +187,8 @@ val named_of_variable_context : variable_context -> Sign.named_context val section_segment_of_constant : Names.constant -> variable_context val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context -val section_instance : Libnames.global_reference -> Names.identifier array -val is_in_section : Libnames.global_reference -> bool +val section_instance : Globnames.global_reference -> Names.identifier array +val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.identifier -> Decl_kinds.binding_kind -> unit @@ -201,7 +201,7 @@ val replacement_context : unit -> val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant -val discharge_global : Libnames.global_reference -> Libnames.global_reference +val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive diff --git a/library/libnames.ml b/library/libnames.ml index 24f083887..37ae97ace 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -10,123 +10,6 @@ open Pp open Errors open Util open Names -open Nameops -open Term -open Mod_subst - -(*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 - -let isVarRef = function VarRef _ -> true | _ -> false -let isConstRef = function ConstRef _ -> true | _ -> false -let isIndRef = function IndRef _ -> true | _ -> false -let isConstructRef = function ConstructRef _ -> true | _ -> false - -let eq_gr gr1 gr2 = - match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 - | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2 - | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2 - | _,_ -> gr1=gr2 - -let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" -let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" -let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" -let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" - -let subst_constructor subst ((kn,i),j as ref) = - let kn' = subst_ind subst kn in - if kn==kn' then ref, mkConstruct ref - else ((kn',i),j), mkConstruct ((kn',i),j) - -let subst_global subst ref = match ref with - | VarRef var -> ref, mkVar var - | ConstRef kn -> - let kn',t = subst_con subst kn in - if kn==kn' then ref, mkConst kn else ConstRef kn', t - | IndRef (kn,i) -> - let kn' = subst_ind subst kn in - if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i) - | ConstructRef ((kn,i),j as c) -> - let c',t = subst_constructor subst c in - 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) - | VarRef id -> VarRef id - -let global_of_constr c = match kind_of_term c with - | Const sp -> ConstRef sp - | Ind ind_sp -> IndRef ind_sp - | Construct cstr_cp -> ConstructRef cstr_cp - | Var id -> VarRef id - | _ -> raise Not_found - -let constr_of_global = function - | VarRef id -> mkVar id - | ConstRef sp -> mkConst sp - | ConstructRef sp -> mkConstruct sp - | IndRef sp -> mkInd sp - -let constr_of_reference = constr_of_global -let reference_of_constr = global_of_constr - -let global_ord_gen fc fmi x y = - let ind_ord (indx,ix) (indy,iy) = - let c = Pervasives.compare ix iy in - if c = 0 then kn_ord (fmi indx) (fmi indy) else c - in - match x, y with - | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy) - | IndRef indx, IndRef indy -> ind_ord indx indy - | ConstructRef (indx,jx), ConstructRef (indy,jy) -> - let c = Pervasives.compare jx jy in - if c = 0 then ind_ord indx indy else c - | _, _ -> Pervasives.compare x y - -let global_ord_can = global_ord_gen canonical_con canonical_mind -let global_ord_user = global_ord_gen user_con user_mind - -(* By default, [global_reference] are ordered on their canonical part *) - -module RefOrdered = struct - type t = global_reference - let compare = global_ord_can -end - -module RefOrdered_env = struct - type t = global_reference - let compare = global_ord_user -end - -module Refset = Set.Make(RefOrdered) -module Refmap = Map.Make(RefOrdered) - -(* Extended global references *) - -type syndef_name = kernel_name - -type extended_global_reference = - | TrueGlobal of global_reference - | SynDef of syndef_name - -(* We order [extended_global_reference] via their user part - (cf. pretty printer) *) - -module ExtRefOrdered = struct - type t = extended_global_reference - let compare x y = - match x, y with - | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry - | SynDef knx, SynDef kny -> kn_ord knx kny - | _, _ -> Pervasives.compare x y -end (**********************************************) @@ -236,32 +119,6 @@ let restrict_path n sp = let dir' = list_firstn n (repr_dirpath dir) in make_path (make_dirpath dir') s -let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id) - -let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) - -let decode_mind kn = - let rec dir_of_mp = function - | MPfile dir -> repr_dirpath dir - | MPbound mbid -> - let _,_,dp = repr_mbid mbid in - let id = id_of_mbid mbid in - id::(repr_dirpath dp) - | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp) - in - let mp,sec_dir,l = repr_mind kn in - if (repr_dirpath sec_dir) = [] then - (make_dirpath (dir_of_mp mp)),id_of_label l - else - anomaly "Section part should be empty!" - -let decode_con kn = - let mp,sec_dir,l = repr_con kn in - match mp,(repr_dirpath sec_dir) with - MPfile dir,[] -> (dir,id_of_label l) - | _ , [] -> anomaly "MPfile expected!" - | _ -> anomaly "Section part should be empty!" - (*s qualified names *) type qualid = full_path @@ -295,14 +152,6 @@ type global_dir_reference = | DirClosedSection of dir_path (* this won't last long I hope! *) -(* | ModRef mp -> - let mp' = subst_modpath subst mp in if mp==mp' then ref else - ModRef mp' - | ModTypeRef kn -> - let kn' = subst_kernel_name subst kn in if kn==kn' then ref else - ModTypeRef kn' -*) - type reference = | Qualid of qualid located | Ident of identifier located @@ -317,28 +166,12 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> pr_id id + | Ident (_,id) -> str (string_of_id id) let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc -(* popping one level of section in global names *) - -let pop_con con = - let (mp,dir,l) = repr_con con in - Names.make_con 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 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 "VarRef not poppable" - (* Deprecated synonyms *) let make_short_qualid = qualid_of_ident diff --git a/library/libnames.mli b/library/libnames.mli index d3eed0364..0fe687343 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -10,69 +10,6 @@ open Pp open Errors open Util open Names -open Term -open Mod_subst - -(** {6 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 - -val isVarRef : global_reference -> bool -val isConstRef : global_reference -> bool -val isIndRef : global_reference -> bool -val isConstructRef : global_reference -> bool - -val eq_gr : global_reference -> global_reference -> bool -val canonical_gr : global_reference -> global_reference - -val destVarRef : global_reference -> variable -val destConstRef : global_reference -> constant -val destIndRef : global_reference -> inductive -val destConstructRef : global_reference -> constructor - - -val subst_constructor : substitution -> constructor -> constructor * constr -val subst_global : substitution -> global_reference -> global_reference * constr - -(** Turn a global reference into a construction *) -val constr_of_global : global_reference -> constr - -(** Turn a construction denoting a global reference into a global reference; - raise [Not_found] if not a global reference *) -val global_of_constr : constr -> global_reference - -(** Obsolete synonyms for constr_of_global and global_of_constr *) -val constr_of_reference : global_reference -> constr -val reference_of_constr : constr -> global_reference - -module RefOrdered : sig - type t = global_reference - val compare : global_reference -> global_reference -> int -end - -module RefOrdered_env : sig - type t = global_reference - val compare : global_reference -> global_reference -> int -end - -module Refset : Set.S with type elt = global_reference -module Refmap : Map.S with type key = global_reference - -(** {6 Extended global references } *) - -type syndef_name = kernel_name - -type extended_global_reference = - | TrueGlobal of global_reference - | SynDef of syndef_name - -module ExtRefOrdered : sig - type t = extended_global_reference - val compare : t -> t -> int -end (** {6 Dirpaths } *) val pr_dirpath : dir_path -> Pp.std_ppcmds @@ -121,14 +58,6 @@ module Spmap : Map.S with type key = full_path val restrict_path : int -> full_path -> full_path -(** {6 Temporary function to brutally form kernel names from section paths } *) - -val encode_mind : dir_path -> identifier -> mutual_inductive -val decode_mind : mutual_inductive -> dir_path * identifier -val encode_con : dir_path -> identifier -> constant -val decode_con : constant -> dir_path * identifier - - (** {6 ... } *) (** A [qualid] is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial @@ -184,12 +113,6 @@ val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc -(** {6 Popping one level of section in global names } *) - -val pop_con : constant -> constant -val pop_kn : mutual_inductive-> mutual_inductive -val pop_global_reference : global_reference -> global_reference - (** Deprecated synonyms *) val make_short_qualid : identifier -> qualid (** = qualid_of_ident *) diff --git a/library/library.mllib b/library/library.mllib index edd5bfc07..e3916900f 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,5 +1,6 @@ Nameops Libnames +Globnames Libobject Summary Nametab diff --git a/library/nametab.ml b/library/nametab.ml index 42edb156f..2bdd71cc4 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -12,6 +12,7 @@ open Compat open Pp open Names open Libnames +open Globnames open Nameops open Declarations diff --git a/library/nametab.mli b/library/nametab.mli index 5183abbe8..fe59ffad6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -11,6 +11,7 @@ open Util open Pp open Names open Libnames +open Globnames (** This module contains the tables for globalization. *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3ac5b87ba..3263de8d5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -19,7 +19,6 @@ open Vernacexpr open Locality open Decl_kinds open Genarg -open Ppextend open Goptions open Declaremods open Misctypes diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 50270f863..7387f6933 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -16,6 +16,7 @@ open Glob_term open Genarg open Tacexpr open Libnames +open Globnames open Nametab open Detyping diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 226ef4b36..27ca281c8 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -14,15 +14,10 @@ Dyn Hashcons Predicate Option -Hashtbl_alt Names Univ -Esubst -Term -Mod_subst -Nameops Libnames Summary Genarg diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ba3def1a0..4034252db 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -19,7 +19,6 @@ open Topconstr open Genarg open Tacexpr open Extrawit -open Ppextend (** The parser of Coq *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 6e9f475a3..15acfd718 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -89,7 +89,7 @@ let pr_located pr (loc,x) = pr x let pr_evaluable_reference = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) + | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -314,7 +314,7 @@ let pr_ltac_constant sp = let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> - Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) + Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) let pr_esubst prc l = let pr_qhyp = function diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f1f6db64d..f4c53333f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -29,6 +29,7 @@ open Libobject open Printer open Printmod open Libnames +open Globnames open Nametab open Recordops open Misctypes diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 122da7ebf..d6bec7162 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -15,6 +15,7 @@ open Term open Environ open Reductionops open Libnames +open Globnames open Nametab open Misctypes diff --git a/parsing/printer.ml b/parsing/printer.ml index a932a608f..8754b9129 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -17,6 +17,7 @@ open Environ open Global open Declare open Libnames +open Globnames open Nametab open Evd open Proof_type diff --git a/parsing/printer.mli b/parsing/printer.mli index bbc3a6cad..77e4db79e 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -9,6 +9,7 @@ open Pp open Names open Libnames +open Globnames open Term open Sign open Environ diff --git a/parsing/printmod.ml b/parsing/printmod.ml index cf047bfa3..d81802ac2 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -12,6 +12,7 @@ open Util open Names open Declarations open Nameops +open Globnames open Libnames open Goptions diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index cb4fad6f5..7467a32f0 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,7 +8,6 @@ open Pp open Names -open Libnames open Q_util open Compat @@ -39,8 +38,8 @@ let mlexpr_of_dirpath dir = <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >> let mlexpr_of_qualid qid = - let (dir, id) = repr_qualid qid in - <:expr< make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> + let (dir, id) = Libnames.repr_qualid qid in + <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 58d809bdb..0f89f348e 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -2,7 +2,7 @@ let contrib_name = "btauto" let init_constant dir s = let find_constant contrib dir s = - Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + Globnames.constr_of_global (Coqlib.find_reference contrib dir s) in find_constant contrib_name dir s @@ -10,7 +10,7 @@ let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in - Lazy.lazy_from_fun (fun () -> Libnames.destIndRef (glob_ref ())) + Lazy.lazy_from_fun (fun () -> Globnames.destIndRef (glob_ref ())) let decomp_term (c : Term.constr) = Term.kind_of_term (Term.strip_outer_cast c) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 7c097c6d6..6d3a5be39 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -157,7 +157,7 @@ let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) +let _eq = Globnames.constr_of_global (Coqlib.glob_eq) let decompose_eq env id = let typ = Environ.named_type id env in @@ -247,7 +247,7 @@ let rec glob_of_pat = add_params (pred n) (GHole(dummy_loc, Evar_kinds.TomatchTypeParameter(ind,n))::q) in let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), + glob_app(loc,GRef(dummy_loc,Globnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function @@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rind = GRef (dummy_loc,Globnames.IndRef pinfo.per_ind) in let rparams = List.map detype_ground pinfo.per_params in let rparams_rec = List.map diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 820da1c3c..2d069b497 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -505,7 +505,7 @@ let instr_cut mkstat _thus _then cut gls0 = (* iterated equality *) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) +let _eq = Globnames.constr_of_global (Coqlib.glob_eq) let decompose_eq id gls = let typ = pf_get_hyp_typ gls id in diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 1b443f753..0f0b902c3 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -15,6 +15,7 @@ open Declarations open Namegen open Nameops open Libnames +open Globnames open Table open Miniml open Mlutil diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 02a496bec..a081d74ae 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Miniml open Mlutil open Pp diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index aa536b1dc..2c845ce32 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -10,6 +10,7 @@ open Term open Declarations open Names open Libnames +open Globnames open Pp open Errors open Util diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index e587bf212..c846d2d0f 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -10,6 +10,7 @@ open Names open Libnames +open Globnames val simple_extraction : reference -> unit val full_extraction : string option -> reference list -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d9ee92c05..2533e3a39 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -21,7 +21,7 @@ open Inductiveops open Recordops open Namegen open Summary -open Libnames +open Globnames open Nametab open Miniml open Table diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index fe249cd65..a8fb02993 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -14,6 +14,7 @@ open Util open Names open Nameops open Libnames +open Globnames open Table open Miniml open Mlutil diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index a5b57a474..f96447c15 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -12,7 +12,7 @@ open Pp open Errors open Util open Names -open Libnames +open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f03170948..3221909bc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -12,6 +12,7 @@ open Errors open Util open Names open Libnames +open Globnames open Nametab open Table open Miniml diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 630db6f06..30f1df45d 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -10,7 +10,7 @@ open Errors open Util open Names open Term -open Libnames +open Globnames open Miniml open Table diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 6380ee7ec..bfaecd0f0 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -9,7 +9,7 @@ open Names open Declarations open Environ -open Libnames +open Globnames open Errors open Util open Miniml diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 0565522bf..29a0fb44f 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -9,7 +9,7 @@ open Names open Declarations open Environ -open Libnames +open Globnames open Miniml open Mod_subst diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d99bca6f4..61759dc24 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -13,7 +13,7 @@ open Errors open Util open Names open Nameops -open Libnames +open Globnames open Table open Miniml open Mlutil diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 667182480..ecedc9002 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,6 +15,7 @@ open Summary open Libobject open Goptions open Libnames +open Globnames open Errors open Util open Pp diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a3b7124e1..7505664a6 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -8,6 +8,7 @@ open Names open Libnames +open Globnames open Miniml open Declarations diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 566b2b8b0..7633cc144 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,7 @@ open Tacmach open Errors open Util open Declarations -open Libnames +open Globnames open Inductiveops let qflag=ref true diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 379aaff18..b3120735c 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -8,7 +8,7 @@ open Term open Names -open Libnames +open Globnames val qflag : bool ref diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a45d3075f..bc15cb501 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -24,7 +24,7 @@ open Declarations open Formula open Sequent open Names -open Libnames +open Globnames open Misctypes let compare_instance inst1 inst2= @@ -40,11 +40,11 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else Libnames.RefOrdered.compare id1 id2 + else Globnames.RefOrdered.compare id1 id2 module OrderedInstance= struct - type t=instance * Libnames.global_reference + type t=instance * Globnames.global_reference let compare (inst1,id1) (inst2,id2)= (compare_instance =? compare_gr) inst2 inst1 id2 id1 (* we want a __decreasing__ total order *) diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index be69b0675..4ad8aa18f 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -9,7 +9,7 @@ open Term open Tacmach open Names -open Libnames +open Globnames open Rules val collect_quantified : Sequent.t -> Formula.t list * Sequent.t diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index a226cc455..fa2b37e96 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -17,7 +17,7 @@ open Termops open Declarations open Formula open Sequent -open Libnames +open Globnames open Locus type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 7d1e57f4a..142a1560b 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -9,7 +9,7 @@ open Term open Tacmach open Names -open Libnames +open Globnames type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 780e3f3e7..269439a53 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -13,7 +13,7 @@ open Formula open Unify open Tacmach open Names -open Libnames +open Globnames open Pp let newcnt ()= @@ -70,7 +70,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - (Libnames.RefOrdered.compare + (Globnames.RefOrdered.compare =? (fun oc1 oc2 -> match oc1,oc2 with Some (m1,c1),Some (m2,c2) -> diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 5587e9fbb..8a2406e36 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -12,7 +12,7 @@ open Util open Formula open Tacmach open Names -open Libnames +open Globnames module OrderedConstr: Set.OrderedType with type t=constr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 1a629aac9..c9760de17 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -17,6 +17,7 @@ open Tactics open Clenv open Names open Libnames +open Globnames open Tacticals open Tacmach open Fourier diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a3bb2eee9..046b65ee8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -15,6 +15,7 @@ open Tacticals open Tactics open Indfun_common open Libnames +open Globnames open Misctypes let msgnl = Pp.msgnl diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b38503cb9..21f77e438 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -101,7 +101,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in let rel_as_kn = fst (match princ_type_info.indref with - | Some (Libnames.IndRef ind) -> ind + | Some (Globnames.IndRef ind) -> ind | _ -> error "Not a valid predicate" ) in @@ -660,7 +660,7 @@ let build_scheme fas = let f_as_constant = try match Nametab.global f with - | Libnames.ConstRef c -> c + | Globnames.ConstRef c -> c | _ -> Errors.error "Functional Scheme can only be used with functions" with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f) @@ -692,7 +692,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try Libnames.constr_of_global (Nametab.global f) + try Globnames.constr_of_global (Nametab.global f) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun = destConst funs in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index cf9b54a94..d1fc8ef33 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -5,6 +5,7 @@ open Term open Glob_term open Glob_ops open Libnames +open Globnames open Indfun_common open Errors open Util @@ -971,7 +972,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in mkGProd(n,t,new_b),id_to_exclude with Continue -> - let jmeq = Libnames.IndRef (destInd (jmeq ())) in + let jmeq = Globnames.IndRef (destInd (jmeq ())) in let ty' = Pretyping.understand Evd.empty env ty in let ind,args' = Inductive.find_inductive env ty' in let mib,_ = Global.lookup_inductive ind in @@ -981,7 +982,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let rt_typ = GApp(Pp.dummy_loc, - GRef (Pp.dummy_loc,Libnames.IndRef ind), + GRef (Pp.dummy_loc,Globnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 6433fe37c..8967a3ec8 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -441,7 +441,7 @@ let rec pattern_to_term = function let patl_as_term = List.map pattern_to_term patternl in - mkGApp(mkGRef(Libnames.ConstructRef constr), + mkGApp(mkGRef(Globnames.ConstructRef constr), implicit_args@patl_as_term ) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 761337b07..437ba225d 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -17,7 +17,7 @@ val pattern_to_term : cases_pattern -> glob_constr Some basic functions to rebuild glob_constr In each of them the location is Util.dummy_loc *) -val mkGRef : Libnames.global_reference -> glob_constr +val mkGRef : Globnames.global_reference -> glob_constr val mkGVar : Names.identifier -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d3f56341f..2a6a7dea3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -5,6 +5,7 @@ open Term open Pp open Indfun_common open Libnames +open Globnames open Glob_term open Declarations open Misctypes diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index c0b72f0b3..654d42ee1 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -23,4 +23,4 @@ val functional_induction : Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma -val make_graph : Libnames.global_reference -> unit +val make_graph : Globnames.global_reference -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index de7e17957..026b9ad0e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,6 +1,7 @@ open Names open Pp open Libnames +open Globnames open Refiner open Hiddentac let mk_prefix pre id = id_of_string (pre^(string_of_id id)) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index bb59a5c9c..8f80c072c 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -117,9 +117,9 @@ val h_intros: Names.identifier list -> Proof_type.tactic val h_id : Names.identifier val hrec_id : Names.identifier val acc_inv_id : Term.constr Util.delayed -val ltof_ref : Libnames.global_reference Util.delayed +val ltof_ref : Globnames.global_reference Util.delayed val well_founded_ltof : Term.constr Util.delayed val acc_rel : Term.constr Util.delayed val well_founded : Term.constr Util.delayed -val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference +val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4d072eca5..b0897c61e 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -13,6 +13,7 @@ open Names open Term open Pp open Libnames +open Globnames open Tacticals open Tactics open Indfun_common diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ebe5cebd2..af7506103 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -9,6 +9,7 @@ (* Merging of induction principles. *) open Libnames +open Globnames open Tactics open Indfun_common open Errors diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0b61c5f85..2005a90e3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -16,6 +16,7 @@ open Entries open Pp open Names open Libnames +open Globnames open Nameops open Errors open Util diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 2c82bab7b..ddaf82a18 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -32,6 +32,7 @@ open Tactics open Clenv open Logic open Libnames +open Globnames open Nametab open Contradiction open Misctypes diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 4bf08912a..ab6ee1573 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -15,6 +15,7 @@ open Flags open Term open Names open Libnames +open Globnames open Nameops open Reductionops open Tacticals @@ -744,7 +745,7 @@ let constants_to_unfold = let transform s = let sp = path_of_string s in let dir, id = repr_path sp in - Libnames.encode_con dir id + Globnames.encode_con dir id in List.map transform [ "Coq.ring.Ring_normalize.interp_cs"; diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 298b24850..c1cea8aac 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -31,11 +31,11 @@ let destructurate t = let c, args = Term.decompose_app t in match Term.kind_of_term c, args with | Term.Const sp, args -> - Kapp (string_of_global (Libnames.ConstRef sp), args) + Kapp (string_of_global (Globnames.ConstRef sp), args) | Term.Construct csp , args -> - Kapp (string_of_global (Libnames.ConstructRef csp), args) + Kapp (string_of_global (Globnames.ConstructRef csp), args) | Term.Ind isp, args -> - Kapp (string_of_global (Libnames.IndRef isp), args) + Kapp (string_of_global (Globnames.IndRef isp), args) | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> @@ -48,9 +48,9 @@ let dest_const_apply t = let f,args = Term.decompose_app t in let ref = match Term.kind_of_term f with - | Term.Const sp -> Libnames.ConstRef sp - | Term.Construct csp -> Libnames.ConstructRef csp - | Term.Ind isp -> Libnames.IndRef isp + | Term.Const sp -> Globnames.ConstRef sp + | Term.Construct csp -> Globnames.ConstructRef csp + | Term.Ind isp -> Globnames.IndRef isp | _ -> raise Destruct in Nametab.basename_of_global ref, args diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 590776760..c2815aafa 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -16,6 +16,7 @@ open Term open Closure open Environ open Libnames +open Globnames open Tactics open Glob_term open Tacticals diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index cf51af134..b2e2e5b19 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -14,13 +14,14 @@ open Pcoq open Glob_term open Topconstr open Libnames +open Globnames open Coqlib open Bigint exception Non_closed_ascii let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let make_kn dir id = Libnames.encode_mind (make_dir dir) (id_of_string id) +let make_kn dir id = Globnames.encode_mind (make_dir dir) (id_of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let ascii_module = ["Coq";"Strings";"Ascii"] diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 984bae418..b67cbb934 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -10,6 +10,7 @@ open Bigint open Libnames +open Globnames open Glob_term (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index b3195f281..f8161c52f 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -13,6 +13,7 @@ open Names open Pcoq open Topconstr open Libnames +open Globnames exception Non_closed_number @@ -31,7 +32,7 @@ let make_path dir id = Libnames.make_path dir (id_of_string id) let r_path = make_path rdefinitions "R" (* TODO: temporary hack *) -let make_path dir id = Libnames.encode_con dir (id_of_string id) +let make_path dir id = Globnames.encode_con dir (id_of_string id) let r_kn = make_path rdefinitions "R" let glob_R = ConstRef r_kn diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 640806d87..ac17492d2 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -12,6 +12,7 @@ open Util open Names open Pcoq open Libnames +open Globnames open Topconstr open Ascii_syntax open Glob_term diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 450d57969..a69ec9ed1 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -22,6 +22,7 @@ exception Non_closed_number (**********************************************************************) open Libnames +open Globnames open Glob_term let binnums = ["Coq";"Numbers";"BinNums"] @@ -32,7 +33,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let positive_path = make_path binnums "positive" (* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_mind dir id +let make_kn dir id = Globnames.encode_mind dir id let positive_kn = make_kn (make_dir binnums) (id_of_string "positive") let glob_positive = IndRef (positive_kn,0) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 78a402898..ec0910d7f 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -125,16 +125,16 @@ let token_list_of_path dir id tag = let token_list_of_kernel_name tag = let module N = Names in - let module LN = Libnames in + let module GN = Globnames in let id,dir = match tag with | Variable kn -> N.id_of_label (N.label kn), Lib.cwd () | Constant con -> N.id_of_label (N.con_label con), - Lib.remove_section_part (LN.ConstRef con) + Lib.remove_section_part (GN.ConstRef con) | Inductive kn -> N.id_of_label (N.mind_label kn), - Lib.remove_section_part (LN.IndRef (kn,0)) + Lib.remove_section_part (GN.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) ;; @@ -431,13 +431,13 @@ print_endline "PASSATO" ; flush stdout ; let subst,residual_args,uninst_vars = let variables,basedir = try - let g = Libnames.global_of_constr h in + let g = Globnames.global_of_constr h in let sp = match g with - Libnames.ConstructRef ((induri,_),_) - | Libnames.IndRef (induri,_) -> - Nametab.path_of_global (Libnames.IndRef (induri,0)) - | Libnames.VarRef id -> + Globnames.ConstructRef ((induri,_),_) + | Globnames.IndRef (induri,_) -> + Nametab.path_of_global (Globnames.IndRef (induri,0)) + | Globnames.VarRef id -> (* Invariant: variables are never cooked in Coq *) raise Not_found | _ -> Nametab.path_of_global g diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 93ff00dff..81dba546e 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -470,15 +470,15 @@ let kind_of_constant kn = ;; let kind_of_global r = - let module Ln = Libnames in + let module Gn = Globnames in match r with - | Ln.IndRef kn | Ln.ConstructRef (kn,_) -> + | Gn.IndRef kn | Gn.ConstructRef (kn,_) -> let isrecord = try let _ = Recordops.lookup_projections kn in Declare.KernelSilent with Not_found -> Declare.KernelVerbose in kind_of_inductive isrecord (fst kn) - | Ln.VarRef id -> kind_of_variable id - | Ln.ConstRef kn -> kind_of_constant kn + | Gn.VarRef id -> kind_of_variable id + | Gn.ConstRef kn -> kind_of_constant kn ;; let print_object_kind uri (xmltag,variation) = @@ -504,12 +504,12 @@ let print internal glob_ref kind xml_library_root = let module Nt = Nametab in let module T = Term in let module X = Xml in - let module Ln = Libnames in + let module Gn = Globnames in (* Variables are the identifiers of the variables in scope *) let variables = search_variables () in let tag,obj = match glob_ref with - Ln.VarRef id -> + Gn.VarRef id -> (* this kn is fake since it is not provided by Coq *) let kn = let (mod_path,dir_path) = Lib.current_prefix () in @@ -517,7 +517,7 @@ let print internal glob_ref kind xml_library_root = in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ - | Ln.ConstRef kn -> + | Gn.ConstRef kn -> let id = N.id_of_label (N.con_label kn) in let cb = G.lookup_constant kn in let val0 = D.body_of_constant cb in @@ -525,14 +525,14 @@ let print internal glob_ref kind xml_library_root = let hyps = cb.D.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps - | Ln.IndRef (kn,_) -> + | Gn.IndRef (kn,_) -> let mib = G.lookup_mind kn in let {D.mind_nparams=nparams; D.mind_packets=packs ; D.mind_hyps=hyps; D.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite - | Ln.ConstructRef _ -> + | Gn.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") in let fn = filename_of_path xml_library_root tag in @@ -580,7 +580,7 @@ let _ = Declare.set_xml_declare_variable (function (sp,kn) -> let id = Libnames.basename sp in - print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ; + print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ; proof_to_export := None) ;; @@ -589,7 +589,7 @@ let _ = (function (internal,kn) -> match !proof_to_export with None -> - print internal (Libnames.ConstRef kn) (kind_of_constant kn) + print internal (Globnames.ConstRef kn) (kind_of_constant kn) xml_library_root | Some pftreestate -> (* It is a proof. Let's export it starting from the proof-tree *) @@ -603,7 +603,7 @@ let _ = let _ = Declare.set_xml_declare_inductive (function (isrecord,(sp,kn)) -> - print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0)) + print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn)) xml_library_root) ;; diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 54ffcd653..43483d2da 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -8,7 +8,7 @@ (*i*) open Names -open Libnames +open Globnames open Decl_kinds open Term open Sign diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a484ecf7f..243bb6b7e 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Environ open Term diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 3be7e7862..cc664f9b5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -12,6 +12,7 @@ open Pp open Flags open Names open Libnames +open Globnames open Nametab open Environ open Libobject diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 66bb5c6c6..dd5214b04 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -29,7 +29,7 @@ type cl_info_typ = { cl_param : int } (** This is the type of coercion kinds *) -type coe_typ = Libnames.global_reference +type coe_typ = Globnames.global_reference (** This is the type of infos for declared coercions *) type coe_info_typ diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c1e0d123d..ab4388047 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -23,6 +23,7 @@ open Nameops open Termops open Namegen open Libnames +open Globnames open Nametab open Evd open Mod_subst diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e49f2b4eb..3fb679067 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -18,7 +18,7 @@ open Termops open Environ open Recordops open Evarutil -open Libnames +open Globnames open Evd type flex_kind_of_term = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5164385ce..0197af56c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -16,6 +16,7 @@ open Termops open Sign open Environ open Libnames +open Globnames open Mod_subst (* The kinds of existential variables are now defined in [Evar_kinds] *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7a48ee9de..b592d7829 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -12,7 +12,7 @@ open Util open Names open Sign open Term -open Libnames +open Globnames open Nametab open Decl_kinds open Misctypes diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index f08b7493c..e9d6a3c29 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -15,6 +15,7 @@ open Errors open Util open Names open Libnames +open Globnames open Nameops open Term open Namegen diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 554face37..0dfb18d84 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -11,7 +11,7 @@ open Pp open Errors open Util open Names -open Libnames +open Globnames open Nameops open Termops open Reductionops diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 9a1425716..f25e6be92 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -19,6 +19,7 @@ open Term open Nametab open Nameops open Libnames +open Globnames open Environ open Termops diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 244d03021..1e73e2634 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -9,7 +9,7 @@ open Errors open Util open Names -open Libnames +open Globnames open Nameops open Term open Glob_term diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 74e5a81ae..c523ce0b2 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -11,7 +11,7 @@ open Names open Sign open Term open Environ -open Libnames +open Globnames open Nametab open Glob_term open Mod_subst diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b241336e7..4eeb50cd0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -35,6 +35,7 @@ open Environ open Type_errors open Typeops open Libnames +open Globnames open Nameops open Classops open List diff --git a/pretyping/program.ml b/pretyping/program.ml index bb0cbe1c7..046379ed6 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -33,7 +33,7 @@ let find_reference locstr dir s = with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp)) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s -let coq_constant locstr dir s = Libnames.constr_of_global (coq_reference locstr dir s) +let coq_constant locstr dir s = Globnames.constr_of_global (coq_reference locstr dir s) let init_constant dir s () = coq_constant "Program" dir s let init_reference dir s () = coq_reference "Program" dir s diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e35004ef1..e2b03d0f2 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -17,7 +17,7 @@ open Errors open Util open Pp open Names -open Libnames +open Globnames open Nametab open Term open Typeops diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 6165fac26..0419ae907 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -9,7 +9,7 @@ open Names open Nametab open Term -open Libnames +open Globnames open Libobject open Library diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 05136d25d..5505a39d3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -13,6 +13,7 @@ open Names open Nameops open Term open Libnames +open Globnames open Termops open Namegen open Declarations diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index c9b139ac9..37531af21 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,7 +15,7 @@ open Closure open Glob_term open Termops open Pattern -open Libnames +open Globnames open Locus type reduction_tactic_error = @@ -29,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Libnames.global_reference -> 'a +val error_not_evaluable : Globnames.global_reference -> 'a val evaluable_of_global_reference : - Environ.env -> Libnames.global_reference -> evaluable_global_reference + Environ.env -> Globnames.global_reference -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Libnames.global_reference + evaluable_global_reference -> Globnames.global_reference exception Redelimination diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 2bf15d2f3..c5ce0f45e 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -12,7 +12,7 @@ open Util open Term open Sign open Names -open Libnames +open Globnames open Mod_subst open Pp (* debug *) (*i*) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 6be28ebcb..d76fdc85d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -8,7 +8,7 @@ (*i*) open Names -open Libnames +open Globnames open Decl_kinds open Term open Sign diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 7e283e56d..6c97516ca 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Decl_kinds open Term open Sign diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index a5ba7e98a..fee55e72a 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -19,7 +19,7 @@ open Constrexpr open Compat open Pp open Util -open Libnames +open Globnames (*i*) type contexts = Parameters | Properties diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 45857df40..925222766 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -17,7 +17,7 @@ open Mod_subst open Constrexpr open Errors open Pp -open Libnames +open Globnames type contexts = Parameters | Properties diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d0782e970..b043b69f6 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,7 +12,7 @@ open Util open Names open Term open Declarations -open Libnames +open Globnames open Genredexpr open Pattern open Reductionops diff --git a/tactics/auto.ml b/tactics/auto.ml index 158221d79..6146998cb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -35,6 +35,7 @@ open Tacticals open Clenv open Hiddentac open Libnames +open Globnames open Nametab open Smartlocate open Libobject diff --git a/tactics/auto.mli b/tactics/auto.mli index 0dfcb0b68..e34141446 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -17,7 +17,7 @@ open Clenv open Pattern open Environ open Evd -open Libnames +open Globnames open Vernacexpr open Mod_subst open Misctypes diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index c13136b95..18ff0a509 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -10,7 +10,7 @@ open Term open Names open Termdn open Pattern -open Libnames +open Globnames (* Discrimination nets with bounded depth. See the module dn.ml for further explanations. diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index bfebf7810..a749ba8ab 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -35,7 +35,7 @@ open Classes open Topconstr open Pfedit open Command -open Libnames +open Globnames open Evd open Compat open Locus diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index fe380db7c..0d16e4931 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -76,7 +76,7 @@ let my_it_mkLambda_or_LetIn_name s c = let get_coq_eq () = try - let eq = Libnames.destIndRef Coqlib.glob_eq in + let eq = Globnames.destIndRef Coqlib.glob_eq in let _ = Global.lookup_inductive eq in (* Do not force the lazy if they are not defined *) mkInd eq, Coqlib.build_coq_eq_refl () diff --git a/tactics/equality.ml b/tactics/equality.ml index cfbb30a74..81457fc9c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -19,6 +19,7 @@ open Inductive open Inductiveops open Environ open Libnames +open Globnames open Reductionops open Typeops open Typing diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4f1174916..5abbe7ae9 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -236,7 +236,7 @@ let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ] let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ] let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] -open Libnames +open Globnames let match_with_equation t = if not (isApp t) then raise NoEquationFound; @@ -489,7 +489,7 @@ let match_eqdec t = false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in match subst with | [(_,typ);(_,c1);(_,c2)] -> - eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ + eqonleft, Globnames.constr_of_global (Lazy.force op), c1, c2, typ | _ -> anomaly "Unexpected pattern" (* Patterns "~ ?" and "? -> False" *) diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index dce518f87..9522a75d9 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -13,7 +13,7 @@ open Term open Libobject open Library open Pattern -open Libnames +open Globnames (* Named, bounded-depth, term-discrimination nets. Implementation: diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index 652ff4f42..9ddb05cd2 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -8,7 +8,7 @@ open Term open Pattern -open Libnames +open Globnames (** Named, bounded-depth, term-discrimination nets. *) module Make : diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 75f6bdb7c..004599f45 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -37,6 +37,7 @@ open Constrexpr open Pfedit open Command open Libnames +open Globnames open Evd open Compat open Misctypes @@ -1736,7 +1737,7 @@ let add_morphism_infer glob m n = (fun () -> Lemmas.start_proof instance_id kind instance (fun _ -> function - Libnames.ConstRef cst -> + Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a0fd61c06..d98167ed0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -26,6 +26,7 @@ open Util open Names open Nameops open Libnames +open Globnames open Nametab open Smartlocate open Pfedit diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 75f0b4a51..bf9353076 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -21,7 +21,7 @@ open Inductive open Inductiveops open Reductionops open Environ -open Libnames +open Globnames open Evd open Pfedit open Tacred diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5cf460366..7294a319d 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -20,7 +20,7 @@ open Evar_refiner open Clenv open Redexpr open Tacticals -open Libnames +open Globnames open Genarg open Tacexpr open Nametab diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 570c6c7a1..79c1797e4 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -11,7 +11,7 @@ open Term open Hipattern open Names -open Libnames +open Globnames open Pp open Proof_type open Tacticals diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 0e7009113..ce7ac29f1 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -14,7 +14,7 @@ open Term open Pattern open Patternops open Glob_term -open Libnames +open Globnames open Nametab (* Discrimination nets of terms. diff --git a/tactics/termdn.mli b/tactics/termdn.mli index c4e747be0..b325a7950 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -8,7 +8,7 @@ open Term open Pattern -open Libnames +open Globnames open Names (** Discrimination nets of terms. *) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 863365800..61bc1ae7c 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -21,7 +21,7 @@ open Declarations open Declare open Term open Names -open Libnames +open Globnames open Goptions open Mod_subst open Indrec diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 1795336f4..a8075294e 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -13,7 +13,7 @@ open Names open Term open Evd open Sign -open Libnames +open Globnames (*i*) (*s @@ -106,7 +106,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let (_,genl,_) = Termops.decompose_prod_letin pat in let genl = List.map (fun (_,_,t) -> t) genl in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in - let def = applistc (Libnames.constr_of_global gr) argl in + let def = applistc (Globnames.constr_of_global gr) argl in (* msgnl(str"essayons ?"++Pp.int ev++spc()++str":="++spc() ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) @@ -214,8 +214,8 @@ let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ct (* main search function: search for total instances containing gr, and apply k to each of them *) let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit = - let gr_c = Libnames.constr_of_global gr in - let (smap:(Libnames.global_reference * Evd.evar_map, + let gr_c = Globnames.constr_of_global gr in + let (smap:(Globnames.global_reference * Evd.evar_map, ('a * 'b * Term.constr) list * Evd.evar) Gmapl.t ref) = ref Gmapl.empty in iter_under_prod diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index dd50cda5a..28a60e516 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -7,7 +7,7 @@ (************************************************************************) open Term -open Libnames +open Globnames open Typeclasses open Names open Evd diff --git a/toplevel/class.ml b/toplevel/class.ml index 9adf68031..4c267ca83 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -22,6 +22,7 @@ open Lib open Classops open Declare open Libnames +open Globnames open Nametab open Decl_kinds open Safe_typing diff --git a/toplevel/class.mli b/toplevel/class.mli index 0e328c1d4..71d096b93 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -10,7 +10,7 @@ open Names open Term open Classops open Declare -open Libnames +open Globnames open Decl_kinds open Nametab diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 593276589..7065bd265 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -22,6 +22,7 @@ open Util open Typeclasses_errors open Typeclasses open Libnames +open Globnames open Constrintern open Glob_term open Constrexpr diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 4ac722eb2..d3be9c016 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -20,6 +20,7 @@ open Util open Typeclasses open Implicit_quantifiers open Libnames +open Globnames (** Errors *) @@ -40,7 +41,7 @@ val declare_instance_constant : int option -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) - ?hook:(Libnames.global_reference -> unit) -> + ?hook:(Globnames.global_reference -> unit) -> identifier -> (** name *) Term.constr -> (** body *) Term.types -> (** type *) @@ -54,7 +55,7 @@ val new_instance : constr_expr option -> ?generalize:bool -> ?tac:Proof_type.tactic -> - ?hook:(Libnames.global_reference -> unit) -> + ?hook:(Globnames.global_reference -> unit) -> int option -> identifier diff --git a/toplevel/command.ml b/toplevel/command.ml index 0cf5aaa68..51d66a761 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -18,6 +18,7 @@ open Redexpr open Declare open Names open Libnames +open Globnames open Nameops open Constrexpr open Constrexpr_ops diff --git a/toplevel/command.mli b/toplevel/command.mli index 005a4a33a..a43f2ad37 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -11,6 +11,7 @@ open Names open Term open Entries open Libnames +open Globnames open Tacexpr open Vernacexpr open Constrexpr diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 640ef4ab5..3fba117a9 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -27,6 +27,7 @@ open Decl_kinds open Indrec open Declare open Libnames +open Globnames open Goptions open Nameops open Termops diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 78aa3fd12..57b623712 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -19,7 +19,7 @@ open Declarations open Entries open Environ open Nameops -open Libnames +open Globnames open Decls open Decl_kinds open Declare diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 2f98962cf..b169b7d1d 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -9,7 +9,7 @@ open Term open Summary open Libobject -open Libnames +open Globnames open Names (* * Module construction @@ -23,16 +23,16 @@ let reduce c = c module TypeDnet = Term_dnet.Make (struct - type t = Libnames.global_reference + type t = Globnames.global_reference let compare = RefOrdered.compare - let subst s gr = fst (Libnames.subst_global s gr) + let subst s gr = fst (Globnames.subst_global s gr) let constr_of = Global.type_of_global end) (struct let reduce = reduce let direction = false end) -type result = Libnames.global_reference * (constr*existential_key) * Termops.subst +type result = Globnames.global_reference * (constr*existential_key) * Termops.subst let all_types = ref TypeDnet.empty let defined_types = ref TypeDnet.empty diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index a6a95ccfc..d3944c180 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -13,7 +13,7 @@ open Term (** results are the reference of the object, together with a context (constr+evar) and a substitution under this context *) -type result = Libnames.global_reference * (constr*existential_key) * Termops.subst +type result = Globnames.global_reference * (constr*existential_key) * Termops.subst (** this is the reduction function used in the indexing process *) val reduce : types -> types diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index b7651edec..b49455221 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -10,8 +10,6 @@ open Errors open Util open Names open Libnames -open Ppextend -open Extend open Tacexpr open Vernacexpr open Notation diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 4b26a979d..5ca9ac9b4 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -3,7 +3,7 @@ open Pp open Environ open Term open Names -open Libnames +open Globnames open Summary open Libobject open Entries @@ -782,7 +782,7 @@ let rec solve_obligation prg num tac = else constant_value (Global.env ()) cst | Evar_kinds.Define opaque -> if not opaque && not transparent then error_not_transp () - else Libnames.constr_of_global gr + else Globnames.constr_of_global gr in if transparent then Auto.add_hints true [string_of_id prg.prg_name] diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index d052cc441..8212afe29 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -14,7 +14,7 @@ open Names open Pp open Util open Tacinterp -open Libnames +open Globnames open Proof_type open Vernacexpr open Decl_kinds diff --git a/toplevel/record.ml b/toplevel/record.ml index 84592f2a7..d78a43990 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -10,7 +10,7 @@ open Pp open Errors open Util open Names -open Libnames +open Globnames open Nameops open Term open Environ diff --git a/toplevel/record.mli b/toplevel/record.mli index e2d56cfd8..259ce48cb 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -12,7 +12,7 @@ open Sign open Vernacexpr open Constrexpr open Impargs -open Libnames +open Globnames (** [declare_projections ref name coers params fields] declare projections of record [ref] (if allowed) using the given [name] as argument, and put them diff --git a/toplevel/search.ml b/toplevel/search.ml index 2213d25f9..e5b2ffbaf 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -21,6 +21,7 @@ open Pattern open Matching open Printer open Libnames +open Globnames open Nametab module SearchBlacklist = @@ -124,7 +125,7 @@ let filter_by_module (module_list:dir_path list) (accept:bool) with No_full_path -> false -let ref_eq = Libnames.encode_mind Coqlib.logic_module (id_of_string "eq"), 0 +let ref_eq = Globnames.encode_mind Coqlib.logic_module (id_of_string "eq"), 0 let c_eq = mkInd ref_eq let gref_eq = IndRef ref_eq diff --git a/toplevel/search.mli b/toplevel/search.mli index 95827d54b..d248a9faa 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -11,7 +11,7 @@ open Names open Term open Environ open Pattern -open Libnames +open Globnames open Nametab (** {6 Search facilities. } *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4c2b2f9b2..2d3886a1d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -25,6 +25,7 @@ open Tacinterp open Command open Goptions open Libnames +open Globnames open Nametab open Vernacexpr open Decl_kinds @@ -135,7 +136,7 @@ let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in match glob_ref with - | Libnames.IndRef i -> + | Globnames.IndRef i -> let {Declarations.mind_nparams = np} , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 5ccf8db88..d869e8854 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -17,6 +17,7 @@ open Term open Environ open Glob_term open Libnames +open Globnames open Nametab open Detyping open Constrintern |