diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 6 | ||||
| -rw-r--r-- | library/lib.ml | 22 | ||||
| -rw-r--r-- | library/library.ml | 22 | ||||
| -rw-r--r-- | library/library.mli | 5 |
4 files changed, 23 insertions, 32 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index dcbc46ab72..154b863fa1 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -73,7 +73,7 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - user_err Pp.(str "Sorry, this table name is already used.") + user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) @@ -216,11 +216,11 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - user_err Pp.(str "Sorry, this option name is already used.") + user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.") with Not_found -> if String.List.mem_assoc (nickname key) !string_table || String.List.mem_assoc (nickname key) !ref_table - then user_err Pp.(str "Sorry, this option name is already used.") + then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.") open Libobject diff --git a/library/lib.ml b/library/lib.ml index 690a4fd53d..9c13cdafdb 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -479,7 +479,24 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst - + +let name_instance inst = + (** FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (** Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map map (Univ.Instance.to_array inst) + let add_section_replacement f g poly hyps = match !sectab with | [] -> () @@ -488,7 +505,8 @@ let add_section_replacement f g poly hyps = let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let inst = Univ.UContext.instance ctx in - let subst, ctx = Univ.abstract_universes ctx in + let nas = name_instance inst in + let subst, ctx = Univ.abstract_universes nas ctx in let args = instance_from_variable_context (List.rev sechyps) in let info = { abstr_ctx = sechyps; diff --git a/library/library.ml b/library/library.ml index 0ff82d7cc4..9b9bd07c93 100644 --- a/library/library.ml +++ b/library/library.ml @@ -611,28 +611,6 @@ let import_module export modl = (************************************************************************) (*s Initializing the compilation of a library. *) -let check_coq_overwriting p id = - let l = DirPath.repr p in - let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then - user_err - (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++ - str "it starts with prefix \"Coq\" which is reserved for the Coq library.") - -let start_library fo = - let ldir0 = - try - let lp = Loadpath.find_load_path (Filename.dirname fo) in - Loadpath.logical lp - with Not_found -> Libnames.default_root_prefix - in - let file = Filename.chop_extension (Filename.basename fo) in - let id = Id.of_string file in - check_coq_overwriting ldir0 id; - let ldir = add_dirpath_suffix ldir0 id in - Declaremods.start_library ldir; - ldir - let load_library_todo f = let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in diff --git a/library/library.mli b/library/library.mli index d5815afc40..d298a371b5 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,11 +38,6 @@ type seg_proofs = Constr.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid list -> unit -(** Start the compilation of a file as a library. The first argument must be - output file, and the - returned path is the associated absolute logical path of the library. *) -val start_library : CUnix.physical_path -> DirPath.t - (** End the compilation of a library and save it to a ".vo" file *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> |