1 files changed, 77 insertions, 60 deletions

diff --git a/library/lib.ml b/library/lib.ml
index e95bb47f27..971089c171 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -9,9 +9,9 @@
 open Pp
 open CErrors
 open Util
+open Names
 open Libnames
 open Globnames
-open Nameops
 open Libobject
 open Context.Named.Declaration
 
@@ -62,7 +62,7 @@ let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn),Leaf o) :: stk ->
-	let id = Names.Label.to_id (Names.label kn) in
+	let id = Names.Label.to_id (Names.KerName.label kn) in
 	  (match classify_object o with
 	     | Dispose -> clean acc stk
 	     | Keep o' ->
@@ -93,12 +93,16 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *)
 
-let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
+let initial_prefix = {
+  obj_dir = default_library;
+  obj_mp  = ModPath.initial;
+  obj_sec = DirPath.empty;
+}
 
 type lib_state = {
-  comp_name   : Names.DirPath.t option;
+  comp_name   : DirPath.t option;
   lib_stk     : library_segment;
-  path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+  path_prefix : object_prefix;
 }
 
 let initial_lib_state = {
@@ -115,10 +119,9 @@ let library_dp () =
 (* [path_prefix] is a pair of absolute dirpath and a pair of current
    module path and relative section path *)
 
-let cwd () = fst !lib_state.path_prefix
-let current_prefix () = snd !lib_state.path_prefix
-let current_mp () = fst (snd !lib_state.path_prefix)
-let current_sections () = snd (snd !lib_state.path_prefix)
+let cwd () = !lib_state.path_prefix.obj_dir
+let current_mp () = !lib_state.path_prefix.obj_mp
+let current_sections () = !lib_state.path_prefix.obj_sec
 
 let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
 let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -136,8 +139,8 @@ let make_path_except_section id =
   Libnames.make_path (cwd_except_section ()) id
 
 let make_kn id =
-  let mp,dir = current_prefix () in
-  Names.make_kn mp dir (Names.Label.of_id id)
+  let mp, dir = current_mp (), current_sections () in
+  Names.KerName.make mp dir (Names.Label.of_id id)
 
 let make_oname id = Libnames.make_oname !lib_state.path_prefix id
 
@@ -152,8 +155,11 @@ let recalc_path_prefix () =
   lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
 
 let pop_path_prefix () =
-  let dir,(mp,sec) = !lib_state.path_prefix in
-  lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
+  let op = !lib_state.path_prefix in
+  lib_state := { !lib_state
+                 with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir;
+                                              obj_sec = pop_dirpath op.obj_sec;
+                                    } }
 
 let find_entry_p p =
   let rec find = function
@@ -226,7 +232,7 @@ let add_anonymous_entry node =
   add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
-  if Names.ModPath.equal (current_mp ()) Names.initial_path then
+  if ModPath.equal (current_mp ()) ModPath.initial then
     user_err Pp.(str "No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -278,14 +284,14 @@ let current_mod_id () =
 
 
 let start_mod is_type export id mp fs =
-  let dir = add_dirpath_suffix (cwd ()) id in
-  let prefix = dir,(mp,Names.DirPath.empty) in
+  let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in
+  let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
     else Nametab.exists_module dir
   in
   if exists then
-    user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
+    user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
   add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
   lib_state := { !lib_state with path_prefix = prefix} ;
   prefix
@@ -296,7 +302,7 @@ let start_modtype = start_mod true None
 let error_still_opened string oname =
   let id = basename (fst oname) in
   user_err 
-    (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
+    (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.")
 
 let end_mod is_type =
   let oname,fs =
@@ -328,17 +334,17 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !lib_state.comp_name != None then
     user_err Pp.(str "compilation unit is already started");
-  if not (Names.DirPath.is_empty (current_sections ())) then
+  if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then
     user_err Pp.(str "some sections are already opened");
-  let prefix = s, (mp, Names.DirPath.empty) in
-  let () = add_anonymous_entry (CompilingLibrary prefix) in
+  let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+  add_anonymous_entry (CompilingLibrary prefix);
   lib_state := { !lib_state with comp_name = Some s;
                                  path_prefix = prefix }
 
 let open_blocks_message es =
   let open_block_name = function
-      | oname, OpenedSection _ -> str "section " ++ pr_id (basename (fst oname))
-      | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ pr_id (basename (fst oname))
+      | oname, OpenedSection _ -> str "section " ++ Id.print (basename (fst oname))
+      | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ Id.print (basename (fst oname))
       | _ -> assert false in
   str "The " ++ pr_enum open_block_name es ++ spc () ++
   str "need" ++ str (if List.length es == 1 then "s" else "") ++ str " to be closed."
@@ -360,8 +366,8 @@ let end_compilation_checks dir =
       | None -> anomaly (Pp.str "There should be a module name...")
       | Some m ->
 	  if not (Names.DirPath.equal m dir) then anomaly
-	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
-             spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
+           (str "The current open module has name" ++ spc () ++ DirPath.print m ++
+             spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str ".");
   in
   oname
 
@@ -395,7 +401,7 @@ let find_opening_node id =
     let id' = basename (fst oname) in
     if not (Names.Id.equal id id') then
       user_err ~hdr:"Lib.find_opening_node"
-        (str "Last block to end has name " ++ pr_id id' ++ str ".");
+        (str "Last block to end has name " ++ Id.print id' ++ str ".");
     entry
   with Not_found -> user_err Pp.(str "There is nothing to end.")
 
@@ -411,14 +417,17 @@ let find_opening_node id =
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
-		  
+type abstr_info = {
+  abstr_ctx : variable_context;
+  abstr_subst : Univ.Instance.t;
+  abstr_uctx : Univ.AUContext.t;
+}
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
   | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.universe_context_set)
-  | Context of Univ.universe_context_set
+		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Context of Univ.ContextSet.t
 
 let sectab =
   Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
@@ -477,8 +486,12 @@ let add_section_replacement f g poly hyps =
     let inst = Univ.UContext.instance ctx in
     let subst, ctx = Univ.abstract_universes ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (inst,args) exps,
-	      g (sechyps,subst,ctx) abs)::sl
+    let info = {
+      abstr_ctx = sechyps;
+      abstr_subst = subst;
+      abstr_uctx = ctx;
+    } in
+    sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
 let add_section_kn poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -496,12 +509,21 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let variable_section_segment_of_reference = function
-  | ConstRef con -> pi1 (section_segment_of_constant con)
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      pi1 (section_segment_of_mutual_inductive kn)
-  | _ -> []
-                     
+let empty_segment = {
+  abstr_ctx = [];
+  abstr_subst = Univ.Instance.empty;
+  abstr_uctx = Univ.AUContext.empty;
+}
+
+let section_segment_of_reference = function
+| ConstRef c -> section_segment_of_constant c
+| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+  section_segment_of_mutual_inductive kn
+| VarRef _ -> empty_segment
+
+let variable_section_segment_of_reference gr =
+  (section_segment_of_reference gr).abstr_ctx
+
 let section_instance = function
   | VarRef id ->
      let eq = function
@@ -522,15 +544,15 @@ let is_in_section ref =
 (*************)
 (* Sections. *)
 let open_section id =
-  let olddir,(mp,oldsec) = !lib_state.path_prefix in
-  let dir = add_dirpath_suffix olddir id in
-  let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
-  if Nametab.exists_section dir then
-    user_err ~hdr:"open_section" (pr_id id ++ str " already exists.");
+  let opp = !lib_state.path_prefix in
+  let obj_dir = add_dirpath_suffix opp.obj_dir id in
+  let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+  if Nametab.exists_section obj_dir then
+    user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry (make_oname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+  Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix);
   lib_state := { !lib_state with path_prefix = prefix };
   add_section ()
 
@@ -556,7 +578,7 @@ let close_section () =
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  let full_olddir = fst !lib_state.path_prefix in
+  let full_olddir = !lib_state.path_prefix.obj_dir in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
@@ -596,10 +618,10 @@ let init () =
 (* Misc *)
 
 let mp_of_global = function
-  |VarRef id -> current_mp ()
-  |ConstRef cst -> Names.con_modpath cst
-  |IndRef ind -> Names.ind_modpath ind
-  |ConstructRef constr -> Names.constr_modpath constr
+  | VarRef id -> !lib_state.path_prefix.obj_mp
+  | ConstRef cst -> Names.Constant.modpath cst
+  | IndRef ind -> Names.ind_modpath ind
+  | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp = function
   |Names.MPfile dp -> dp
@@ -621,12 +643,12 @@ let library_part = function
 (* Discharging names *)
 
 let con_defined_in_sec kn =
-  let _,dir,_ = Names.repr_con kn in
+  let _,dir,_ = Names.Constant.repr3 kn in
   not (Names.DirPath.is_empty dir) &&
   Names.DirPath.equal (pop_dirpath dir) (current_sections ())
 
 let defined_in_sec kn =
-  let _,dir,_ = Names.repr_mind kn in
+  let _,dir,_ = Names.MutInd.repr3 kn in
   not (Names.DirPath.is_empty dir) &&
   Names.DirPath.equal (pop_dirpath dir) (current_sections ())
 
@@ -648,15 +670,10 @@ let discharge_con cst =
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
 
-let discharge_abstract_universe_context (_, subst, abs_ctx) auctx =
+let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
   let open Univ in
-  let len = LMap.cardinal subst in
-  let rec gen_subst i acc =
-    if i < 0 then acc
-    else
-      let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
-      gen_subst (pred i) acc
-  in
-  let subst = gen_subst (AUContext.size auctx - 1) subst in
+  let ainst = make_abstract_instance auctx in
+  let subst = Instance.append subst ainst in
+  let subst = make_instance_subst subst in
   let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
   subst, AUContext.union abs_ctx auctx