diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 6 | ||||
| -rw-r--r-- | library/lib.ml | 22 |
2 files changed, 23 insertions, 5 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; |