From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 library/lib.ml | 52 ++++++++++++++++++----------------------------------
 1 file changed, 18 insertions(+), 34 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 543cb45b..8ebe4489 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,13 +26,11 @@ type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
   | OpenedModule of is_type * export * object_prefix * Summary.frozen
-  | ClosedModule  of library_segment
   | OpenedSection of object_prefix * Summary.frozen
-  | ClosedSection of library_segment
 
-and library_entry = object_name * node
+type library_entry = object_name * node
 
-and library_segment = library_entry list
+type library_segment = library_entry list
 
 type lib_objects =  (Names.Id.t * obj) list
 
@@ -51,7 +49,7 @@ let subst_objects subst seg =
       if obj' == obj then node else
 	(id, obj')
   in
-    List.smartmap subst_one seg
+    List.Smart.map subst_one seg
 
 (*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
@@ -73,10 +71,6 @@ let classify_segment seg =
 		 clean ((id,o')::substl, keepl, anticipl) stk
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
-    | (_,ClosedSection _) :: stk -> clean acc stk
-    (* LEM; TODO: Understand what this does and see if what I do is the
-                  correct thing for ClosedMod(ule|type) *)
-    | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
@@ -183,22 +177,11 @@ let split_lib_gen test =
     | before -> after,equal,before
   in
   let rec findeq after = function
-    | hd :: before ->
-      	if test hd
-	then Some (collect after [hd] before)
-	else (match hd with
-		| (sp,ClosedModule  seg)
-		| (sp,ClosedSection seg) ->
-		    (match findeq after seg with
-		       | None -> findeq (hd::after) before
-		       | Some (sub_after,sub_equal,sub_before) ->
-			   Some (sub_after, sub_equal, (List.append sub_before before)))
-		| _ -> findeq (hd::after) before)
-    | [] -> None
+    | hd :: before when test hd -> collect after [hd] before
+    | hd :: before -> findeq (hd::after) before
+    | [] -> user_err Pp.(str "no such entry")
   in
-    match findeq [] !lib_state.lib_stk with
-      | None -> user_err Pp.(str "no such entry")
-      | Some r -> r
+  findeq [] !lib_state.lib_stk
 
 let eq_object_name (fp1, kn1) (fp2, kn2) =
   eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2
@@ -318,7 +301,6 @@ let end_mod is_type =
   in
   let (after,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !lib_state.path_prefix in
   recalc_path_prefix ();
   (oname, prefix, fs, after)
@@ -416,7 +398,7 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
 type abstr_info = {
@@ -566,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | ClosedSection _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
 
@@ -580,13 +561,10 @@ 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 = !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
   Summary.unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
 
@@ -602,10 +580,8 @@ let freeze ~marshallable =
         | n, (CompilingLibrary _ as x) -> Some (n,x)
         | n, OpenedModule (it,e,op,_) ->
                Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
-        | n, ClosedModule _ -> Some (n,ClosedModule [])
         | n, OpenedSection (op, _) ->
-               Some(n,OpenedSection(op,Summary.empty_frozen))
-        | n, ClosedSection _ -> Some (n,ClosedSection []))
+               Some(n,OpenedSection(op,Summary.empty_frozen)))
       !lib_state.lib_stk in
     { !lib_state with lib_stk }
   | _ ->
@@ -669,6 +645,14 @@ let discharge_kn kn =
 let discharge_con cst =
   if con_defined_in_sec cst then Globnames.pop_con cst else cst
 
+let discharge_proj_repr =
+  Projection.Repr.map_npars (fun mind npars ->
+      if not (defined_in_sec mind) then mind, npars
+      else
+        let modlist = replacement_context () in
+        let _, newpars = Mindmap.find mind (snd modlist) in
+        Globnames.pop_kn mind, npars + Array.length newpars)
+
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
 
-- 
cgit v1.2.3