Nouvelle approche pour le discharge modulaire

- Avant : une unique méthode discharge_function qui avait accès à l'ancien
  environnement mais pas de possibilité de raisonner avec les objets
  du nouvel environnement en cours de construction. C'était problématique
  pour le discharge des implicites, arguments scope, etc qui étaient
  finalement faits en même temps que le discharge des constantes et inductifs
  mais avec pour effets de bord que les entrées dans la lib_stk arrivaient 
  juste avant celles des constantes et inductifs avec des problèmes pour
  effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
  pour collecter de l'ancien environnement ce qui est à garder dans la
  section et rebuild_function qui reconstruit le nouvel environnement 
  connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
  ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
  l'extensibilité que la méthode ancienne du fichier discharge.ml ne
  permettait pas)

Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
  
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)

Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 250 insertions, 249 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 446e42d3c..f729f133d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -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 0e7bdef30..2a2e69e91 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -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 1dcbcead8..296e53310 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -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 None 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 local = local or (match ref with VarRef _ -> true | _ -> false) in
+  let req =
+    if local 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 23ed327ba..615861043 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -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 ac710c357..4c822114e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -188,9 +188,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
@@ -373,10 +379,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
@@ -409,16 +422,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
@@ -461,11 +476,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 = 
@@ -479,16 +497,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. *)
diff --git a/library/lib.mli b/library/lib.mli
index 5639ffed7..9f5a3f78a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -166,8 +166,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 424cf1f73..d951b616e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -264,3 +264,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 69710f431..2d5d5258f 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -141,3 +141,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 0a5379ee5..46cc55361 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -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 3d60e48ad..540b69feb 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -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