Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

13 files changed, 277 insertions, 279 deletions

diff --git a/library/declare.ml b/library/declare.ml
index e9e54cd3..02bdb1cf 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 9104 2006-09-01 11:04:44Z notin $ *)
+(* $Id: declare.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -136,7 +136,7 @@ let _ = Summary.declare_summary "CONSTANT"
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn),(_,_,_,kind)) =
+let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant" 
       (pr_id (basename sp) ++ str " already exists");
@@ -147,21 +147,17 @@ let load_constant i ((sp,kn),(_,_,_,kind)) =
 let open_constant i ((sp,kn),_) =
   Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
-let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-    if Idmap.mem id !vartab then
-      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-    if Nametab.exists_cci sp then
-      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-    let kn' = Global.add_constant dir id cdt in
-      assert (kn' = constant_of_kn kn);
-      Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
-      add_section_constant kn' (Global.lookup_constant kn').const_hyps;
-      Dischargedhypsmap.set_discharged_hyps sp dhyps;
-      with_implicits imps declare_constant_implicits kn';
-      Notation.declare_ref_arguments_scope (ConstRef kn');
-      csttab := Spmap.add sp kind !csttab
+  if Idmap.mem id !vartab or Nametab.exists_cci sp then
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+  let kn' = Global.add_constant dir id cdt in
+  assert (kn' = constant_of_kn kn);
+  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+  add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+  Dischargedhypsmap.set_discharged_hyps sp dhyps;
+  csttab := Spmap.add sp kind !csttab
 
 (*s Registration as global tables and rollback. *)
 
@@ -172,18 +168,18 @@ let discharged_hyps kn sechyps =
   let args = array_map_to_list destVar (instance_from_named_context sechyps) in
   List.rev (List.map (Libnames.make_path dir) args)
 
-let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   let con = constant_of_kn kn in
   let cb = Global.lookup_constant con in
-  let (repl1,_ as repl) = replacement_context () in
-  let sechyps = section_segment (ConstRef con) in
+  let repl = replacement_context () in
+  let sechyps = section_segment_of_constant con in
   let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
-  Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind)
+  Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
 
-let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk
+let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
 let export_constant cst = Some (dummy_constant cst)
 
@@ -210,9 +206,10 @@ let hcons_constant_declaration = function
   | cd -> cd
 
 let declare_constant_common id dhyps (cd,kind) =
-  let imps = implicits_flags () in
-  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
+  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,kind)) in
   let kn = constant_of_kn kn in
+  declare_constant_implicits kn;
+  Notation.declare_ref_arguments_scope (ConstRef kn);
   kn
 
 let declare_constant_gen internal id (cd,kind) =
@@ -261,16 +258,16 @@ let check_exists_inductive (sp,_) =
     let (_,id) = repr_path sp in
     errorlabstrm "" (pr_id id ++ str " already exists")
 
-let load_inductive i ((sp,kn),(_,_,mie)) =
+let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists_inductive names;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
 
-let open_inductive i ((sp,kn),(_,_,mie)) =
+let open_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
 
-let cache_inductive ((sp,kn),(dhyps,imps,mie)) =
+let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists_inductive names;
   let id = basename sp in
@@ -279,15 +276,13 @@ let cache_inductive ((sp,kn),(dhyps,imps,mie)) =
   assert (kn'=kn);
   add_section_kn kn (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  with_implicits imps declare_mib_implicits kn;
-  declare_inductive_argument_scopes kn mie;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
-let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
+let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mie = Global.lookup_mind kn in
   let repl = replacement_context () in
-  let sechyps = section_segment (IndRef (kn,0)) in
-  Some (discharged_hyps kn sechyps,imps,
+  let sechyps = section_segment_of_mutual_inductive kn in
+  Some (discharged_hyps kn sechyps,
         Discharge.process_inductive sechyps repl mie)
 
 let dummy_one_inductive_entry mie = {
@@ -298,7 +293,7 @@ let dummy_one_inductive_entry mie = {
 }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry (_,imps,m) = ([],imps,{
+let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
   mind_entry_record = false;
   mind_entry_finite = true;
@@ -318,11 +313,12 @@ let (in_inductive, out_inductive) =
 
 (* for initial declaration *)
 let declare_mind isrecord mie =
-  let imps = implicits_flags () in
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
-  let oname = add_leaf id (in_inductive ([],imps,mie)) in
+  let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in
+  declare_mib_implicits kn;
+  declare_inductive_argument_scopes kn mie;
   !xml_declare_inductive (isrecord,oname);
   oname
 
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 2a3abda8..255f5e75 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dischargedhypsmap.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
+(* $Id: dischargedhypsmap.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Util
 open Libnames
@@ -24,21 +24,9 @@ type discharged_hyps = section_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
-let load_discharged_hyps_map _ (_,(sp,hyps)) = 
+let set_discharged_hyps sp hyps = 
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
-let cache_discharged_hyps_map o =
-  load_discharged_hyps_map 1 o
-
-let (in_discharged_hyps_map, _) =
-  declare_object { (default_object "DISCHARGED-HYPS-MAP") with
-    cache_function = cache_discharged_hyps_map;
-    load_function = load_discharged_hyps_map;
-    export_function = (fun x -> Some x) }
-
-let set_discharged_hyps sp hyps =
- add_anonymous_leaf (in_discharged_hyps_map (sp,hyps))
-
 let get_discharged_hyps sp =
   try
    Spmap.find sp !discharged_hyps_map
diff --git a/library/impargs.ml b/library/impargs.ml
index 67848d8f..8cea4737 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: impargs.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Util
 open Names
@@ -45,7 +45,7 @@ let is_contextual_implicit_args () = !contextual_implicit_args
 
 type implicits_flags = bool * bool * bool
 
-let implicits_flags () = 
+let implicit_flags () = 
   (!implicit_args, !strict_implicit_args, !contextual_implicit_args)
 
 let with_implicits (a,b,c) f x =
@@ -167,12 +167,6 @@ let add_free_rels_until strict bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let my_concrete_name avoid names t = function
-  | Anonymous -> Anonymous, avoid, Anonymous::names
-  | na -> 
-      let id = Termops.next_name_not_occuring false na avoid names t in
-      Name id, id::avoid, Name id::names
-  
 let compute_implicits_gen strict contextual env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
@@ -194,15 +188,50 @@ let compute_implicits_gen strict contextual env t =
 	Array.to_list v
     | _ -> []
 
-let compute_implicits env t =
-  let strict = !strict_implicit_args in
-  let contextual = !contextual_implicit_args in
+let compute_implicits_auto env (_,strict,contextual) t =
   let l = compute_implicits_gen strict contextual env t in
   List.map (function
     | (Name id, Some imp) -> Some (id,imp)
     | (Anonymous, Some _) -> anomaly "Unnamed implicit"
     | _ -> None) l
 
+let compute_implicits env t = compute_implicits_auto env (implicit_flags()) t
+
+let set_implicit id imp =
+  Some (id,match imp with None -> Manual | Some imp -> imp)
+
+let compute_manual_implicits flags ref l =
+  let t = Global.type_of_global ref in
+  let autoimps = compute_implicits_gen false true (Global.env()) t in
+  let n = List.length autoimps in
+  if not (list_distinct l) then 
+    error ("Some parameters are referred more than once");
+  (* Compare with automatic implicits to recover printing data and names *)
+  let rec merge k l = function
+    | (Name id,imp)::imps ->
+	let l',imp =
+	  try list_remove_first (ExplByPos k) l, set_implicit id imp
+	  with Not_found ->
+	  try list_remove_first (ExplByName id) l, set_implicit id imp
+	  with Not_found ->
+	  l, None in
+	imp :: merge (k+1) l' imps
+    | (Anonymous,imp)::imps -> 
+	None :: merge (k+1) l imps
+    | [] when l = [] -> []
+    | _ ->
+	match List.hd l with
+	| ExplByName id ->
+	    error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+	| ExplByPos i ->
+	    if i<1 or i>n then 
+	      error ("Bad implicit argument number: "^(string_of_int i))
+	    else
+	      errorlabstrm ""
+		(str "Cannot set implicit argument number " ++ int i ++
+		 str ": it has no name") in
+  merge 1 l autoimps
+
 type implicit_status =
     (* None = Not implicit *)
     (identifier * implicit_explanation) option
@@ -238,44 +267,18 @@ let positions_of_implicits =
 type strict_flag = bool     (* true = strict *)
 type contextual_flag = bool (* true = contextual *)
 
-type implicits =
-  | Impl_auto of strict_flag * contextual_flag * implicits_list
-  | Impl_manual of implicits_list
-  | No_impl
-
-let auto_implicits env ty =
-  if !implicit_args then
-    let l = compute_implicits env ty in
-    Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
-  else
-    No_impl
-
-let list_of_implicits = function 
-  | Impl_auto (_,_,l) -> l
-  | Impl_manual l -> l
-  | No_impl -> []
-
 (*s Constants. *)
 
-let constants_table = ref Cmap.empty
-
-let compute_constant_implicits cst =
+let compute_constant_implicits flags cst =
   let env = Global.env () in
-  auto_implicits env (Typeops.type_of_constant env cst)
-
-let constant_implicits sp =
-  try Cmap.find sp !constants_table with Not_found -> No_impl
+  compute_implicits_auto env flags (Typeops.type_of_constant env cst)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
    $i$ are the implicit arguments of the inductive and $v$ the array of 
    implicit arguments of the constructors. *)
 
-let inductives_table = ref Indmap.empty
-
-let constructors_table = ref Constrmap.empty
-
-let compute_mib_implicits kn =
+let compute_mib_implicits flags kn =
   let env = Global.env () in
   let mib = lookup_mind kn env in
   let ar =
@@ -288,54 +291,55 @@ let compute_mib_implicits kn =
   let imps_one_inductive i mip =
     let ind = (kn,i) in
     let ar = type_of_inductive env (mib,mip) in
-    ((IndRef ind,auto_implicits env ar),
-     Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
+    ((IndRef ind,compute_implicits_auto env flags ar),
+     Array.mapi (fun j c ->
+       (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c))
        mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
 
-let inductive_implicits indp =
-  try Indmap.find indp !inductives_table with Not_found -> No_impl
-
-let constructor_implicits consp =
-  try Constrmap.find consp !constructors_table with Not_found -> No_impl
+let compute_all_mib_implicits flags kn =
+  let imps = compute_mib_implicits flags kn in
+  List.flatten 
+    (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
 
 (*s Variables. *)
 
-let var_table = ref Idmap.empty
-
-let compute_var_implicits id =
+let compute_var_implicits flags id =
   let env = Global.env () in
   let (_,_,ty) = lookup_named id env in
-  auto_implicits env ty
-
-let var_implicits id = 
-  try Idmap.find id !var_table with Not_found -> No_impl
+  compute_implicits_auto env flags ty
 
 (* Implicits of a global reference. *)
 
-let compute_global_implicits = function
-  | VarRef id -> compute_var_implicits id
-  | ConstRef kn -> compute_constant_implicits kn
+let compute_global_implicits flags = function
+  | VarRef id -> compute_var_implicits flags id
+  | ConstRef kn -> compute_constant_implicits flags kn
   | IndRef (kn,i) -> 
-      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+      let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps
   | ConstructRef ((kn,i),j) -> 
-      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
+      let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
 
 (* Caching implicits *)
 
-let cache_implicits_decl (r,imps) =
-  match r with
-  | VarRef id -> 
-      var_table := Idmap.add id imps !var_table
-  | ConstRef kn ->
-      constants_table := Cmap.add kn imps !constants_table
-  | IndRef indp ->
-      inductives_table := Indmap.add indp imps !inductives_table;
-  | ConstructRef consp -> 
-      constructors_table := Constrmap.add consp imps !constructors_table
+type implicit_interactive_request = ImplAuto | ImplManual of explicitation list
+
+type implicit_discharge_request =
+  | ImplNoDischarge
+  | ImplConstant of constant * implicits_flags
+  | ImplMutualInductive of kernel_name * implicits_flags
+  | ImplInteractive of global_reference * implicits_flags * 
+      implicit_interactive_request
 
-let load_implicits _ (_,l) = List.iter cache_implicits_decl l
+let implicits_table = ref Refmap.empty
+
+let implicits_of_global ref =
+  try Refmap.find ref !implicits_table with Not_found -> []
+
+let cache_implicits_decl (ref,imps) =
+  implicits_table := Refmap.add ref imps !implicits_table
+
+let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l
 
 let cache_implicits o =
   load_implicits 1 o
@@ -343,121 +347,88 @@ let cache_implicits o =
 let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
-let subst_implicits (_,subst,l) =
-  list_smartmap (subst_implicits_decl subst) l
-
-let (in_implicits, _) =
+let subst_implicits (_,subst,(req,l)) =
+  (ImplNoDischarge,list_smartmap (subst_implicits_decl subst) l)
+
+let discharge_implicits (_,(req,l)) =
+  match req with
+  | ImplNoDischarge -> None
+  | ImplInteractive (ref,flags,exp) -> 
+      Some (ImplInteractive (pop_global_reference ref,flags,exp),l)
+  | ImplConstant (con,flags) ->
+      Some (ImplConstant (pop_con con,flags),l)
+  | ImplMutualInductive (kn,flags) ->
+      Some (ImplMutualInductive (pop_kn kn,flags),l)
+
+let rebuild_implicits (req,l) =
+  let l' = match req with
+  | ImplNoDischarge -> assert false
+  | ImplConstant (con,flags) -> 
+      [ConstRef con,compute_constant_implicits flags con]
+  | ImplMutualInductive (kn,flags) ->
+      compute_all_mib_implicits flags kn
+  | ImplInteractive (ref,flags,o) ->
+      match o with
+      | ImplAuto -> [ref,compute_global_implicits flags ref]
+      | ImplManual l ->
+	  error "Discharge of global manually given implicit arguments not implemented" in
+  (req,l')
+
+
+let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with 
     cache_function = cache_implicits;
     load_function = load_implicits;
     subst_function = subst_implicits;
     classify_function = (fun (_,x) -> Substitute x);
+    discharge_function = discharge_implicits;
+    rebuild_function = rebuild_implicits;
     export_function = (fun x -> Some x) }
 
-let declare_implicits_gen r = 
-  add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
+let declare_implicits_gen req flags ref =
+  let imps = compute_global_implicits flags ref in
+  add_anonymous_leaf (inImplicits (req,[ref,imps]))
 
-let declare_implicits r =
-  with_implicits
-    (true,!strict_implicit_args,!contextual_implicit_args)
-    declare_implicits_gen r
+let declare_implicits local ref =
+  let flags = (true,!strict_implicit_args,!contextual_implicit_args) in
+  let req = 
+    if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in
+  declare_implicits_gen req flags ref
 
 let declare_var_implicits id =
-  if !implicit_args then declare_implicits_gen (VarRef id)
+  if !implicit_args then
+    declare_implicits_gen ImplNoDischarge (implicit_flags ()) (VarRef id)
 
-let declare_constant_implicits kn =
-  if !implicit_args then declare_implicits_gen (ConstRef kn)
+let declare_constant_implicits con =
+  if !implicit_args then
+    let flags = implicit_flags () in
+    declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
 
 let declare_mib_implicits kn =
   if !implicit_args then
-  let imps = compute_mib_implicits kn in
-  let imps = array_map_to_list
-    (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
-  add_anonymous_leaf (in_implicits (List.flatten imps))
-
-let implicits_of_global_gen = function
-  | VarRef id -> var_implicits id
-  | ConstRef sp -> constant_implicits sp
-  | IndRef isp -> inductive_implicits isp
-  | ConstructRef csp ->	constructor_implicits csp
-
-let implicits_of_global r =
-  list_of_implicits (implicits_of_global_gen r)
+    let flags = implicit_flags () in
+    let imps = array_map_to_list
+      (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
+      (compute_mib_implicits flags kn) in
+    add_anonymous_leaf
+      (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
 
 (* Declare manual implicits *)
 
-let set_implicit id imp =
-  Some (id,match imp with None -> Manual | Some imp -> imp)
-
-let declare_manual_implicits r l =
-  let t = Global.type_of_global r in
-  let autoimps = compute_implicits_gen false true (Global.env()) t in
-  let n = List.length autoimps in
-  if not (list_distinct l) then 
-    error ("Some parameters are referred more than once");
-  (* Compare with automatic implicits to recover printing data and names *)
-  let rec merge k l = function
-    | (Name id,imp)::imps ->
-	let l',imp =
-	  try list_remove_first (ExplByPos k) l, set_implicit id imp
-	  with Not_found ->
-	  try list_remove_first (ExplByName id) l, set_implicit id imp
-	  with Not_found ->
-	  l, None in
-	imp :: merge (k+1) l' imps
-    | (Anonymous,imp)::imps -> 
-	None :: merge (k+1) l imps
-    | [] when l = [] -> []
-    | _ ->
-	match List.hd l with
-	| ExplByName id ->
-	    error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
-	| ExplByPos i ->
-	    if i<1 or i>n then 
-	      error ("Bad implicit argument number: "^(string_of_int i))
-	    else
-	      errorlabstrm ""
-		(str "Cannot set implicit argument number " ++ int i ++
-		 str ": it has no name") in
-  let l = Impl_manual (merge 1 l autoimps) in
-  add_anonymous_leaf (in_implicits [r,l])
-
-(* Tests if declared implicit *)
-
-let test = function
-  | No_impl | Impl_manual _ -> false,false,false
-  | Impl_auto (s,c,_) -> true,s,c
-
-let test_if_implicit find a =
-  try let b = find a in test b
-  with Not_found -> (false,false,false)
-    
-let is_implicit_constant sp =
-  test_if_implicit (Cmap.find sp) !constants_table
-
-let is_implicit_inductive_definition indp =
-  test_if_implicit (Indmap.find (indp,0)) !inductives_table
-
-let is_implicit_var id =
-  test_if_implicit (Idmap.find id) !var_table
+let declare_manual_implicits local ref l =
+  let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in
+  let l' = compute_manual_implicits flags ref l in
+  let req =
+    if local or isVarRef ref then ImplNoDischarge
+    else ImplInteractive(ref,flags,ImplManual l)
+  in
+  add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 (*s Registration as global tables *)
 
-let init () =
-  constants_table := Cmap.empty;
-  inductives_table := Indmap.empty;
-  constructors_table := Constrmap.empty;
-  var_table := Idmap.empty
-
-let freeze () =
-  (!constants_table, !inductives_table, 
-   !constructors_table, !var_table)
-
-let unfreeze (ct,it,const,vt) =
-  constants_table := ct;
-  inductives_table := it;
-  constructors_table := const;
-  var_table := vt
+let init () = implicits_table := Refmap.empty
+let freeze () = !implicits_table
+let unfreeze t = implicits_table := t
 
 let _ = 
   Summary.declare_summary "implicits"
diff --git a/library/impargs.mli b/library/impargs.mli
index 671d195c..64ce0360 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: impargs.mli 9488 2007-01-17 11:11:58Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -51,17 +51,10 @@ val declare_var_implicits : variable -> unit
 val declare_constant_implicits : constant -> unit
 val declare_mib_implicits : mutual_inductive -> unit
 
-val declare_implicits : global_reference -> unit
+val declare_implicits : bool -> global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
-val declare_manual_implicits : global_reference -> 
+val declare_manual_implicits : bool -> global_reference -> 
   Topconstr.explicitation list -> unit
 
-(* Get implicit arguments *)
-val is_implicit_constant : constant -> implicits_flags
-val is_implicit_inductive_definition : mutual_inductive -> implicits_flags
-val is_implicit_var : variable -> implicits_flags
-
 val implicits_of_global : global_reference -> implicits_list
-
-val implicits_flags : unit -> implicits_flags
diff --git a/library/lib.ml b/library/lib.ml
index 09200a5c..213a1d19 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 9133 2006-09-12 14:52:07Z notin $ *)
+(* $Id: lib.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -186,9 +186,15 @@ let add_leaf id obj =
   if fst (current_prefix ()) = initial_path then 
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
-    cache_object (oname,obj);
-    add_entry oname (Leaf obj);
-    oname
+  cache_object (oname,obj);
+  add_entry oname (Leaf obj);
+  oname
+
+let add_discharged_leaf id obj =
+  let oname = make_oname id in
+  let newobj = rebuild_object obj in
+  cache_object (oname,newobj);
+  add_entry oname (Leaf newobj)
 
 let add_leaves id objs =
   let oname = make_oname id in
@@ -371,10 +377,17 @@ let what_is_opened () = find_entry_p is_something_opened
 
 (* Discharge tables *)
 
+(* At each level of section, we remember
+   - the list of variables in this section
+   - the list of variables on which each constant depends in this section
+   - the list of variables on which each inductive depends in this section
+   - the list of substitution to do at section closing 
+*)
+
+type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
+
 let sectab =
-  ref ([] : (identifier list *
-             (identifier array Cmap.t * identifier array KNmap.t) *
-             (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list)
+  ref ([] : (identifier list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
@@ -407,16 +420,18 @@ let add_section_constant kn =
 
 let replacement_context () = pi2 (List.hd !sectab)
 
-let section_segment = function
-  | VarRef id ->
-      []
-  | ConstRef con -> 
-      Cmap.find con (fst (pi3 (List.hd !sectab)))
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      KNmap.find kn (snd (pi3 (List.hd !sectab)))
+let section_segment_of_constant con =
+  Cmap.find con (fst (pi3 (List.hd !sectab)))
+
+let section_segment_of_mutual_inductive kn =
+  KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let section_instance r =
-  Sign.instance_from_named_context (List.rev (section_segment r))
+let section_instance = function
+  | VarRef id -> [||]
+  | ConstRef con ->
+      Cmap.find con (fst (pi2 (List.hd !sectab)))
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
 let init () = sectab := []
 let freeze () = !sectab
@@ -459,11 +474,14 @@ let open_section id =
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
 
-let discharge_item = function
-  | ((sp,_ as oname),Leaf lobj) ->
+let discharge_item ((sp,_ as oname),e) =
+  match e with
+  | Leaf lobj ->
       option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | _ ->
-      None
+  | FrozenState _ -> None
+  | ClosedSection -> None
+  | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
+      anomaly "discharge_item"
 
 let close_section id =
   let oname,fs = 
@@ -477,16 +495,16 @@ let close_section id =
       error "no opened section"
   in
   let (secdecls,_,before) = split_lib oname in
-    lib_stk := before;
-    let full_olddir = fst !path_prefix in
-      pop_path_prefix ();
-      add_entry (make_oname id) ClosedSection;
-      if !Options.xml_export then !xml_close_section id;
-      let newdecls = List.map discharge_item secdecls in
-	Summary.section_unfreeze_summaries fs;
-	List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
-	Cooking.clear_cooking_sharing ();
-	Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+  lib_stk := before;
+  let full_olddir = fst !path_prefix in
+  pop_path_prefix ();
+  add_entry (make_oname id) ClosedSection;
+  if !Options.xml_export then !xml_close_section id;
+  let newdecls = List.map discharge_item secdecls in
+  Summary.section_unfreeze_summaries fs;
+  List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
+  Cooking.clear_cooking_sharing ();
+  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
 (*****************)
 (* Backtracking. *)
@@ -660,14 +678,6 @@ let remove_section_part ref =
 (************************)
 (* Discharging names *)
 
-let pop_kn kn =
-  let (mp,dir,l) = Names.repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
-
-let pop_con con = 
-  let (mp,dir,l) = Names.repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
-
 let con_defined_in_sec kn = 
   let _,dir,_ = repr_con kn in
   dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
diff --git a/library/lib.mli b/library/lib.mli
index e33c3aca..ec896de5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 8852 2006-05-23 17:52:43Z notin $ i*)
+(*i $Id: lib.mli 9488 2007-01-17 11:11:58Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -160,8 +160,10 @@ val set_xml_close_section : (identifier -> unit) -> unit
 
 (*s Section management for discharge *)
 
-val section_segment : global_reference -> Sign.named_context
-val section_instance : global_reference -> Term.constr array
+val section_segment_of_constant : constant -> Sign.named_context
+val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
+
+val section_instance : global_reference -> identifier array
 
 val add_section_variable : identifier -> unit
 val add_section_constant : constant -> Sign.named_context -> unit
diff --git a/library/libnames.ml b/library/libnames.ml
index 48a7565e..07c9ad23 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*)
+(*i $Id: libnames.ml 9488 2007-01-17 11:11:58Z herbelin $ i*)
 
 open Pp
 open Util
@@ -21,6 +21,8 @@ type global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
+let isVarRef = function VarRef _ -> true | _ -> false
+
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
@@ -264,3 +266,18 @@ let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
 
+(* popping one level of section in global names *)
+
+let pop_con con =
+  let (mp,dir,l) = repr_con con in
+  Names.make_con mp (dirpath_prefix dir) l
+
+let pop_kn kn =
+  let (mp,dir,l) = repr_kn kn in
+  Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_global_reference = function
+  | ConstRef con -> ConstRef (pop_con con)
+  | IndRef (kn,i) -> IndRef (pop_kn kn,i)
+  | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
+  | VarRef id -> anomaly "VarRef not poppable"
diff --git a/library/libnames.mli b/library/libnames.mli
index ab2185a6..9bf6918e 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli 8768 2006-04-28 14:25:31Z notin $ i*)
+(*i $Id: libnames.mli 9488 2007-01-17 11:11:58Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -23,6 +23,8 @@ type global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
+val isVarRef : global_reference -> bool
+
 val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)
@@ -141,3 +143,9 @@ val qualid_of_reference : reference -> qualid located
 val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
 val loc_of_reference : reference -> loc
+
+(* popping one level of section in global names *)
+
+val pop_con : constant -> constant
+val pop_kn : kernel_name -> kernel_name
+val pop_global_reference : global_reference -> global_reference
diff --git a/library/libobject.ml b/library/libobject.ml
index 709fb1bb..eaaa1be1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 9104 2006-09-01 11:04:44Z notin $ *)
+(* $Id: libobject.ml 9488 2007-01-17 11:11:58Z herbelin $ *)
 
 open Util
 open Names
@@ -37,6 +37,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -50,6 +51,7 @@ let default_object s = {
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
   discharge_function = (fun _ -> None);
+  rebuild_function = (fun x -> x);
   export_function = (fun _ -> None)} 
 
 
@@ -75,6 +77,7 @@ type dynamic_object_declaration = {
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : object_name * obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
+  dyn_rebuild_function : obj -> obj;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -112,6 +115,9 @@ let declare_object odecl =
       option_map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
+  and rebuild lobj = 
+    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
+    else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
       option_map infun (odecl.export_function (outfun lobj))
@@ -125,6 +131,7 @@ let declare_object odecl =
 			     dyn_subst_function = substituter;
 			     dyn_classify_function = classifier;
 			     dyn_discharge_function = discharge;
+			     dyn_rebuild_function = rebuild;
                              dyn_export_function = exporter };
   (infun,outfun)
 
@@ -166,5 +173,8 @@ let classify_object ((_,lobj) as node) =
 let discharge_object ((_,lobj) as node) = 
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
+let rebuild_object lobj =
+  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 88a12db9..376da1f5 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libobject.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id: libobject.mli 9488 2007-01-17 11:11:58Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -71,6 +71,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -105,4 +106,5 @@ val subst_object : object_name * substitution * obj -> obj
 val classify_object : object_name * obj -> obj substitutivity
 val export_object : obj -> obj option
 val discharge_object : object_name * obj -> obj option
+val rebuild_object : obj -> obj
 val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index 43eeb695..b68c3eb5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 9352 2006-11-07 16:12:10Z notin $ *)
+(* $Id: library.ml 9637 2007-02-10 08:32:28Z notin $ *)
 
 open Pp
 open Util
@@ -300,7 +300,7 @@ let (in_import, out_import) =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number = 080999 (* V8.1gamma *)
+let vo_magic_number = 080100 (* V8.1 *)
 
 let (raw_extern_library, raw_intern_library) =
   System.raw_extern_intern vo_magic_number ".vo"
@@ -591,6 +591,12 @@ let current_deps () =
 let current_reexports () =
   List.map (fun m -> m.library_name) !libraries_exports_list
 
+let error_recursively_dependent_library dir =
+  errorlabstrm ""
+    (str "Unable to use logical name" ++ spc() ++ pr_dirpath dir ++ spc() ++ 
+     str "to save current library" ++ spc() ++ str"because" ++ spc() ++ 
+     str "it already depends on a library of this name.")
+
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
   let md = { 
@@ -599,6 +605,8 @@ let save_library_to dir f =
     md_objects = seg;
     md_deps = current_deps ();
     md_imports = current_reexports () } in
+  if List.mem_assoc dir md.md_deps then
+    error_recursively_dependent_library dir;
   let (f',ch) = raw_extern_library f in
   try
     System.marshal_out ch md;
diff --git a/library/nameops.ml b/library/nameops.ml
index 779f3389..6d0ad8ef 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *)
+(* $Id: nameops.ml 9429 2006-12-12 08:01:03Z herbelin $ *)
 
 open Pp
 open Util
@@ -20,8 +20,6 @@ let pr_name = function
   | Anonymous -> str "_"
   | Name id -> pr_id id
 
-let wildcard = id_of_string "_"
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -163,10 +161,7 @@ let next_name_away_with_default default name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> next_ident_away (id_of_string default) l
 
-let next_name_away name l = 
-  match name with
-    | Name str  -> next_ident_away str l
-    | Anonymous -> id_of_string "_"
+let next_name_away = next_name_away_with_default "H"
 
 let pr_lab l = str (string_of_label l)
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 8e291761..25c4ea56 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nameops.mli 9225 2006-10-09 15:59:23Z herbelin $ i*)
+(*i $Id: nameops.mli 9429 2006-12-12 08:01:03Z herbelin $ i*)
 
 open Names
 
@@ -14,8 +14,6 @@ open Names
 val pr_id : identifier -> Pp.std_ppcmds
 val pr_name : name -> Pp.std_ppcmds
 
-val wildcard : identifier
-
 val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option