diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 4 | ||||
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/globnames.ml | 6 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 4 | ||||
| -rw-r--r-- | library/nametab.mli | 2 |
9 files changed, 18 insertions, 13 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 04a6e159eb..82d1ecacb5 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -45,7 +45,7 @@ let has_ref s = CString.Map.mem s !table let check_ind_ref s ind = match CString.Map.find s !table with - | GlobRef.IndRef r -> eq_ind r ind + | GlobRef.IndRef r -> Ind.CanOrd.equal r ind | _ -> false | exception Not_found -> false @@ -84,7 +84,7 @@ let gen_reference_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in let all = Nametab.locate_all qualid in - let all = List.sort_uniquize GlobRef.Ordered_env.compare all in + let all = List.sort_uniquize GlobRef.UserOrd.compare all in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> x diff --git a/library/global.ml b/library/global.ml index 5c847fda96..71cadb3600 100644 --- a/library/global.ml +++ b/library/global.ml @@ -105,9 +105,9 @@ let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) -let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d) let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d) -let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) +let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) diff --git a/library/global.mli b/library/global.mli index 2767594171..c9b9d7f536 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,10 +52,12 @@ val export_private_constants : Safe_typing.exported_private_constant list val add_constant : + ?typing_flags:Declarations.typing_flags -> Id.t -> Safe_typing.global_declaration -> Constant.t val add_private_constant : Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : + ?typing_flags:Declarations.typing_flags -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) @@ -134,7 +136,7 @@ val body_of_constant_body : Opaqueproof.indirect_accessor -> val start_library : DirPath.t -> ModPath.t val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t -> - ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library + ModPath.t * Safe_typing.compiled_library * Nativelib.native_library val import : Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> ModPath.t diff --git a/library/globnames.ml b/library/globnames.ml index bc24fbf096..654349dea0 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -98,14 +98,14 @@ module ExtRefOrdered = struct let equal x y = x == y || match x, y with - | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.equal rx ry | SynDef knx, SynDef kny -> KerName.equal knx kny | (TrueGlobal _ | SynDef _), _ -> false let compare x y = if x == y then 0 else match x, y with - | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.compare rx ry | SynDef knx, SynDef kny -> KerName.compare knx kny | TrueGlobal _, SynDef _ -> -1 | SynDef _, TrueGlobal _ -> 1 @@ -113,7 +113,7 @@ module ExtRefOrdered = struct open Hashset.Combine let hash = function - | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr) + | TrueGlobal gr -> combinesmall 1 (GlobRef.UserOrd.hash gr) | SynDef kn -> combinesmall 2 (KerName.hash kn) end diff --git a/library/lib.ml b/library/lib.ml index 830777003b..fa0a95d366 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -525,8 +525,8 @@ let init () = let mp_of_global = let open GlobRef in function | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst - | IndRef ind -> Names.ind_modpath ind - | ConstructRef constr -> Names.constr_modpath constr + | IndRef ind -> Names.Ind.modpath ind + | ConstructRef constr -> Names.Construct.modpath constr let rec dp_of_mp = function |Names.MPfile dp -> dp diff --git a/library/libnames.ml b/library/libnames.ml index 88b2e41855..ba1ef1e2f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in make_qualid ?loc l a +let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v + let qualid_is_ident qid = DirPath.is_empty qid.CAst.v.dirpath diff --git a/library/libnames.mli b/library/libnames.mli index a384510879..65aca0c87d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid val qualid_of_path : ?loc:Loc.t -> full_path -> qualid val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid +val qualid_of_lident : lident -> qualid val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t diff --git a/library/nametab.ml b/library/nametab.ml index a51c281f2b..d5cc4f8ac5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe ?loc kn = +let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc ctx sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index 8a8b59733c..fa27dcab9a 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) |