Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

14 files changed, 302 insertions, 147 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 07810e3c..4bdc11c3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 10840 2008-04-23 21:29:34Z herbelin $ *)
+(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (** This module is about the low-level declaration of logical objects *)
 
@@ -57,10 +57,12 @@ let cache_variable ((sp,_),o) =
   let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
-        impl, true, cst, (if keep then Some ty else None)
+	let impl = if impl then Lib.Implicit else Lib.Explicit in
+	let keep = if keep then Some ty else None in
+	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
-        false, opaq, cst, None in
+        Lib.Explicit, opaq, cst, None in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl keep;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -116,7 +118,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
-  let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+  let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev (List.map (Libnames.make_path dir) args)
 
 let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
@@ -124,7 +126,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   let cb = Global.lookup_constant 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
+  let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -235,7 +237,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let repl = replacement_context () in
   let sechyps = section_segment_of_mutual_inductive kn in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive sechyps repl mie)
+        Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 123417a6..b630b5dc 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
+(*i $Id: declaremods.ml 11246 2008-07-22 15:10:05Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -433,10 +433,12 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
 			 mod_entry_expr = 
 			      Some (MSEident mp')},sub),
 		    substobjs, match mbids with
-		      | [] -> 
+		      | [] -> let subst = update_subst subst' (map_mp mp' mp) in
 			  Some (subst_objects (dir,(mp',empty_dirpath)) 
-				  (join subst' (join (map_msid msid mp')
-						  (map_mp mp mp'))) objs)
+				  (join (join subst' subst) (join (map_msid msid mp')
+						  (map_mp mp mp')))
+				   objs)
+			    
 		      | _ -> None)
 		     
 	      | _ -> anomaly "Modops: Not an alias"
diff --git a/library/heads.ml b/library/heads.ml
index 626f1795..970ae87b 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heads.ml 10841 2008-04-24 07:19:57Z herbelin $ *)
+(* $Id: heads.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Pp
 open Util
@@ -158,7 +158,7 @@ let discharge_head (_,(ref,k)) =
   | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
   | EvalVarRef id -> None
 
-let rebuild_head (info,(ref,k)) =
+let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
 let export_head o = Some o
diff --git a/library/impargs.ml b/library/impargs.ml
index cae1986e..3a505ddb 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 10796 2008-04-15 12:00:50Z herbelin $ *)
+(* $Id: impargs.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -20,13 +20,14 @@ open Libobject
 open Lib
 open Nametab
 open Pp
-open Termops
 open Topconstr
+open Termops
 
 (*s Flags governing the computation of implicit arguments *)
 
 type implicits_flags = {
   main : bool;
+  manual : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
   strongly_strict : bool;            (* true = strongly strict *)
   reversible_pattern : bool;
@@ -38,6 +39,7 @@ type implicits_flags = {
 
 let implicit_args = ref { 
   main = false;
+  manual = false;
   strict = true;
   strongly_strict = false;
   reversible_pattern = false;
@@ -48,6 +50,10 @@ let implicit_args = ref {
 let make_implicit_args flag =
   implicit_args := { !implicit_args with main = flag }
 
+let make_manual_implicit_args flag =
+  implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
+    manual = flag }
+
 let make_strict_implicit_args flag =
   implicit_args := { !implicit_args with strict = flag }
 
@@ -64,6 +70,7 @@ let make_maximal_implicit_args flag =
   implicit_args := { !implicit_args with maximal = flag }
 
 let is_implicit_args () = !implicit_args.main
+let is_manual_implicit_args () = !implicit_args.manual
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -88,7 +95,7 @@ let set_maximality imps b =
 
 (*s Computation of implicit arguments *)
 
-(* We remember various information about why an argument is (automatically)
+(* We remember various information about why an argument is
    inferable as implicit
 
 - [DepRigid] means that the implicit argument can be found by
@@ -105,6 +112,8 @@ let set_maximality imps b =
   inferable following a rigid path (useful to know how to print a
   partial application)
 
+- [Manual] means the argument has been explicitely set as implicit.
+
   We also consider arguments inferable from the conclusion but it is
   operational only if [conclusion_matters] is true.
 *)
@@ -117,7 +126,7 @@ type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
-  | Manual of bool
+  | Manual
 
 let argument_less = function
   | Hyp n, Hyp n' -> n<n'
@@ -137,7 +146,7 @@ let update pos rig (na,st) =
       | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
-      | Some (Manual _) -> assert false
+      | Some Manual -> assert false
   else
     match st with
       | None -> DepFlex pos
@@ -147,7 +156,7 @@ let update pos rig (na,st) =
           if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
       | Some (DepFlex fpos as x) ->
           if argument_less (pos,fpos) then DepFlex pos else x
-      | Some (Manual _) -> assert false
+      | Some Manual -> assert false
   in na, Some e
 
 (* modified is_rigid_reference with a truncated env *)
@@ -241,11 +250,7 @@ let compute_implicits_flags env f all t =
     f.reversible_pattern f.contextual all env t
     
 let set_implicit id imp insmax =
-  (id,(match imp with None -> Manual false | Some imp -> imp),insmax)
-
-let merge_imps f = function 
-    None -> Some (Manual f)
-  | x -> x
+  (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
 let rec assoc_by_pos k = function
     (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl
@@ -262,7 +267,7 @@ let compute_manual_implicits env flags t enriching l =
       let (id, (b, f)), l' = assoc_by_pos k l in
 	if f then
 	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
-	    l', Some (id,Manual f,b)
+	    l', Some (id,Manual,b)
 	else l, None
     with Not_found -> l, None
   in
@@ -274,11 +279,11 @@ let compute_manual_implicits env flags t enriching l =
       let l',imp,m =
 	try 
 	  let (b, f) = List.assoc (ExplByName id) l in
-	  List.remove_assoc (ExplByName id) l, merge_imps f imp,Some b
+	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some b)
 	with Not_found ->
 	try 
 	  let (id, (b, f)), l' = assoc_by_pos k l in
-	    l', merge_imps f imp,Some b
+	    l', (Some Manual), (Some b)
 	with Not_found ->
 	  l,imp, if enriching && imp <> None then Some flags.maximal else None
       in
@@ -305,11 +310,15 @@ let compute_manual_implicits env flags t enriching l =
   in
   merge 1 l autoimps
 
+let const v _ = v
+
 let compute_implicits_auto env f manual t =
   match manual with
-      [] -> let l = compute_implicits_flags env f false t in
-	      prepare_implicits f l
-    | _ -> compute_manual_implicits env f t true manual
+  | [] -> 
+      let l = compute_implicits_flags env f false t in
+	if f.manual then List.map (const None) l
+	else prepare_implicits f l
+  | _ -> compute_manual_implicits env f t (not f.manual) manual
 	
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
@@ -333,10 +342,6 @@ let maximal_insertion_of = function
   | Some (_,_,b) -> b
   | None -> anomaly "Not an implicit argument"
 
-let forced_implicit = function
-  | Some (_,Manual b,_) -> b
-  | _ -> false
-
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
   | None -> false
@@ -346,7 +351,7 @@ let is_inferable_implicit in_ctx n = function
   | Some (_,DepRigid Conclusion,_) -> in_ctx
   | Some (_,DepFlex Conclusion,_) -> false
   | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual _,_) -> true
+  | Some (_,Manual,_) -> true
 
 let positions_of_implicits =
   let rec aux n = function
@@ -417,9 +422,18 @@ let list_split_at index l =
     | [] -> failwith "list_split_at: Invalid argument"
   in aux 0 [] l
     
-let merge_impls oimpls impls =
-  let oimpls, _ = list_split_at (List.length oimpls - List.length impls) oimpls in
-    oimpls @ impls
+let merge_impls oldimpls newimpls =
+  let (before, news), olds = 
+    let len = List.length newimpls - List.length oldimpls in
+      if len >= 0 then list_split_at len newimpls, oldimpls
+      else 
+	let before, after = list_split_at (-len) oldimpls in
+	  (before, newimpls), after
+  in
+    before @ (List.map2 (fun orig ni ->
+      match orig with
+      | Some (_, Manual, _) -> orig
+      | _ -> ni) olds news)
 
 (* Caching implicits *)
 
@@ -453,34 +467,67 @@ let subst_implicits_decl subst (r,imps as o) =
 let subst_implicits (_,subst,(req,l)) =
   (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
 
+let impls_of_context ctx =
+  List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None)
+    (List.filter (fun (_,_,b,_) -> b = None) ctx)
+
+let section_segment_of_reference = function
+  | ConstRef con -> section_segment_of_constant con
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      section_segment_of_mutual_inductive kn
+  | _ -> []
+
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) -> 
-      Some (ImplInteractive (pop_global_reference ref,flags,exp),l)
+      let vars = section_segment_of_reference ref in
+      let ref' = pop_global_reference ref in
+      let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
+      Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
-      Some (ImplConstant (pop_con con,flags),l)
+      let con' = pop_con con in
+      let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
+	Some (ImplConstant (con',flags),l')
   | ImplMutualInductive (kn,flags) ->
-      Some (ImplMutualInductive (pop_kn kn,flags),l)
+      let l' = List.map (fun (gr, l) -> 
+	let vars = section_segment_of_reference gr in
+	  (pop_global_reference gr, impls_of_context vars @ l)) l 
+      in
+	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
-let rebuild_implicits (info,(req,l)) =
-  let manual = List.fold_left (fun acc (id, impl, keep) -> 
-    if impl then (ExplByName id, (true, true)) :: acc else acc)
-    [] info
-  in
+let rebuild_implicits (req,l) =
   let l' = match req with
   | ImplLocal -> assert false
   | ImplConstant (con,flags) -> 
-      [ConstRef con, compute_constant_implicits flags manual con]
+      let oldimpls = snd (List.hd l) in
+      let newimpls = compute_constant_implicits flags [] con in
+      [ConstRef con, merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
-      compute_all_mib_implicits flags manual kn
+      let newimpls = compute_all_mib_implicits flags [] kn in
+      let rec aux olds news = 
+	match olds, news with
+	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+	    (gr, merge_impls oldimpls newimpls) :: aux old tl
+	| [], [] -> []
+	| _, _ -> assert false
+      in aux l newimpls
+
   | ImplInteractive (ref,flags,o) ->
       match o with
-      | ImplAuto -> [ref,compute_global_implicits flags manual ref]
-      | ImplManual l -> 
-	  let auto = compute_global_implicits flags manual ref in
-(* 	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in *)
-	  let l' = merge_impls auto l in [ref,l']
+      | ImplAuto -> 
+	  let oldimpls = snd (List.hd l) in
+	  let newimpls = compute_global_implicits flags [] ref in
+	    [ref,merge_impls oldimpls newimpls]
+      | ImplManual m -> 
+	  let oldimpls = snd (List.hd l) in
+	  let auto = 
+	    if flags.main then
+	      let newimpls = compute_global_implicits flags [] ref in
+		merge_impls oldimpls newimpls
+	    else oldimpls
+	  in
+	  let l' = merge_impls auto m in [ref,l']
   in (req,l')
 
 let export_implicits (req,_ as x) = 
@@ -545,6 +592,12 @@ let maybe_declare_manual_implicits local ref enriching l =
   if l = [] then ()
   else declare_manual_implicits local ref enriching l
 
+let lift_implicits n = 
+  List.map (fun x -> 
+    match fst x with 
+	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
+      | _ -> x)
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index 5b55af82..705efd31 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 10741 2008-04-02 15:47:07Z msozeau $ i*)
+(*i $Id: impargs.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -20,6 +20,7 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
+val make_manual_implicit_args : bool -> unit
 val make_strict_implicit_args : bool -> unit
 val make_strongly_strict_implicit_args : bool -> unit
 val make_reversible_pattern_implicit_args : bool -> unit
@@ -27,6 +28,7 @@ val make_contextual_implicit_args : bool -> unit
 val make_maximal_implicit_args : bool -> unit
 
 val is_implicit_args : unit -> bool
+val is_manual_implicit_args : unit -> bool
 val is_strict_implicit_args : unit -> bool
 val is_strongly_strict_implicit_args : unit -> bool
 val is_reversible_pattern_implicit_args : unit -> bool
@@ -38,16 +40,25 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
-type implicit_status
-type implicits_list = implicit_status list
 
-type implicit_explanation
+
+type argument_position =
+  | Conclusion
+  | Hyp of int
+
+type implicit_explanation =
+  | DepRigid of argument_position
+  | DepFlex of argument_position
+  | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+  | Manual
+
+type implicit_status = (identifier * implicit_explanation * bool) option
+type implicits_list = implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> identifier
 val maximal_insertion_of : implicit_status -> bool
-val forced_implicit : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
@@ -83,3 +94,30 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
+
+val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
+
+val merge_impls : implicits_list -> implicits_list -> implicits_list
+
+type implicit_interactive_request =
+  | ImplAuto
+  | ImplManual of implicit_status list
+
+type implicit_discharge_request =
+  | ImplLocal
+  | ImplConstant of constant * implicits_flags
+  | ImplMutualInductive of kernel_name * implicits_flags
+  | ImplInteractive of global_reference * implicits_flags * 
+      implicit_interactive_request
+
+val discharge_implicits :     'a *
+    (implicit_discharge_request *
+     (Libnames.global_reference *
+      (Names.identifier * implicit_explanation * bool) option list)
+     list) ->
+    (implicit_discharge_request *
+     (Libnames.global_reference *
+      (Names.identifier * implicit_explanation * bool) option list)
+     list)
+    option
+
diff --git a/library/lib.ml b/library/lib.ml
index ce3d2520..fa71bb2f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *)
+(* $Id: lib.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Pp
 open Util
@@ -214,9 +214,9 @@ let add_leaf id obj =
   add_entry oname (Leaf obj);
   oname
 
-let add_discharged_leaf id varinfo obj =
+let add_discharged_leaf id obj =
   let oname = make_oname id in
-  let newobj = rebuild_object (varinfo, obj) in
+  let newobj = rebuild_object obj in
   cache_object (oname,newobj);
   add_entry oname (Leaf newobj)
 
@@ -436,11 +436,14 @@ let what_is_opened () = find_entry_p is_something_opened
    - the list of variables on which each inductive depends in this section
    - the list of substitution to do at section closing 
 *)
+type binding_kind = Explicit | Implicit
 
-type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
+type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
@@ -451,25 +454,34 @@ let add_section_variable id impl keep =
     | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
 let rec extract_hyps = function
-  | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
+  | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
+  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
   | (id::idl,hyps) -> extract_hyps (idl,hyps)
   | [], _ -> []
 
+let instance_from_variable_context sign =
+  let rec inst_rec = function
+    | (id,b,None,_) :: sign -> id :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
+
+let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
+
 let add_section_replacement f g hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
     let sechyps = extract_hyps (vars,hyps) in
-    let args = Sign.instance_from_named_context (List.rev sechyps) in
-    sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+    let args = instance_from_variable_context (List.rev sechyps) in
+    sectab := (vars,f args exps,g sechyps abs)::sl
 	
 let add_section_kn kn =
-  let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+  let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
   add_section_replacement f f
 
 let add_section_constant kn =
-  let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
   add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
@@ -482,13 +494,22 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
+let rec list_mem_assoc_in_triple x = function
+    [] -> raise Not_found
+  | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
+
 let section_instance = function
-  | VarRef id -> [||]
+  | VarRef id ->
+      if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
+      else raise Not_found
   | ConstRef con ->
       Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
+let is_in_section ref =
+  try ignore (section_instance ref); true with Not_found -> false
+
 let init_sectab () = sectab := []
 let freeze_sectab () = !sectab
 let unfreeze_sectab s = sectab := s
@@ -551,10 +572,6 @@ let close_section id =
     with Not_found ->
       error "no opened section"
   in
-  let var_info = List.map
-    (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
-    (variables_context ())
-  in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
@@ -563,7 +580,7 @@ let close_section id =
   if !Flags.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 var_info o)) newdecls;
+  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)
 
diff --git a/library/lib.mli b/library/lib.mli
index 64074cfd..d35fcc09 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 11046 2008-06-03 22:48:06Z msozeau $ i*)
+(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -171,17 +171,24 @@ val reset_initial : unit -> unit
 val set_xml_open_section : (identifier -> unit) -> unit
 val set_xml_close_section : (identifier -> unit) -> unit
 
+type binding_kind = Explicit | Implicit
 
 (*s Section management for discharge *)
+type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
 
-val section_segment_of_constant : constant -> Sign.named_context
-val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
+val instance_from_variable_context : variable_context -> Names.identifier array
+val named_of_variable_context : variable_context -> Sign.named_context
 
-val section_instance : global_reference -> identifier array
+val section_segment_of_constant : Names.constant -> variable_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
 
-val add_section_variable : identifier -> bool -> Term.types option -> unit
-val add_section_constant : constant -> Sign.named_context -> unit
-val add_section_kn : kernel_name -> Sign.named_context -> unit
+val section_instance : Libnames.global_reference -> Names.identifier array
+val is_in_section : Libnames.global_reference -> bool
+
+val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit
+val add_section_constant : Names.constant -> Sign.named_context -> unit
+val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
   (identifier array Cmap.t * identifier array KNmap.t)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 31822da4..d0c6e8b9 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 10580 2008-02-22 13:39:13Z lmamane $ i*)
+(*i $Id: libnames.ml 11209 2008-07-05 10:17:49Z herbelin $ i*)
 
 open Pp
 open Util
@@ -89,6 +89,8 @@ let drop_dirpath_prefix d1 d2 =
   let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
     make_dirpath (List.rev d)
 
+let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1)
+
 (* To know how qualified a name should be to be understood in the current env*)
 let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
 
diff --git a/library/libnames.mli b/library/libnames.mli
index d4942061..76c406db 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 10308 2007-11-09 09:40:21Z herbelin $ i*)
+(*i $Id: libnames.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -59,6 +59,7 @@ val chop_dirpath : int -> dir_path -> dir_path * dir_path
 val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
 val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+val append_dirpath : dir_path -> dir_path -> dir_path
 
 module Dirset : Set.S with type elt = dir_path
 module Dirmap : Map.S with type key = dir_path
diff --git a/library/libobject.ml b/library/libobject.ml
index ff78f527..6b302447 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 10741 2008-04-02 15:47:07Z msozeau $ *)
+(* $Id: libobject.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -28,8 +28,6 @@ let relax b = relax_flag := b;;
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
-type discharge_info = (identifier * bool * bool) list
-
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
@@ -38,7 +36,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 : discharge_info * 'a -> 'a;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -52,7 +50,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);
+  rebuild_function = (fun x -> x);
   export_function = (fun _ -> None)} 
 
 
@@ -78,7 +76,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 : discharge_info * obj -> obj;
+  dyn_rebuild_function : obj -> obj;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -116,8 +114,8 @@ 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 (varinfo,lobj) = 
-    if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
+  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 
@@ -174,7 +172,7 @@ 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) as node) =
+let rebuild_object (lobj as node) =
   apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
 
 let export_object lobj =
diff --git a/library/libobject.mli b/library/libobject.mli
index 5f6cf13b..4ec5746b 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 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: libobject.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -71,8 +71,6 @@ open Mod_subst
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
-type discharge_info = (identifier * bool * bool) list
-
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
@@ -81,7 +79,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 : discharge_info * 'a -> 'a;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -116,5 +114,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 : discharge_info * obj -> obj
+val rebuild_object : obj -> obj
 val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index 2904edc2..73928a9b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11181 2008-06-27 07:35:45Z notin $ *)
+(* $Id: library.ml 11313 2008-08-07 11:15:03Z barras $ *)
 
 open Pp
 open Util
@@ -25,9 +25,9 @@ open Declaremods
 
 type logical_path = dir_path
 
-let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
 
-let get_load_paths () = fst !load_paths
+let get_load_paths () = List.map pi1 !load_paths
 
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p = 
@@ -57,12 +57,12 @@ let canonical_path_name p =
     (* We give up to find a canonical name and just simplify it... *)
     strip_path p
 
-let find_logical_path phys_dir = 
+let find_logical_path phys_dir =
   let phys_dir = canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
-  | _,[dir] -> dir
-  | _,[] -> Nameops.default_root_prefix
-  | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+  match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
+  | [_,dir,_] -> dir
+  | [] -> Nameops.default_root_prefix
+  | l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let is_in_load_paths phys_dir =
   let dir = canonical_path_name phys_dir in
@@ -71,12 +71,12 @@ let is_in_load_paths phys_dir =
     List.exists check_p lp 
 
 let remove_load_path dir =
-  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+  load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
 
-let add_load_path (phys_path,coq_path) =
+let add_load_path isroot (phys_path,coq_path) =
   let phys_path = canonical_path_name phys_path in
-    match list_filter2 (fun p d -> p = phys_path) !load_paths with
-      | _,[dir] ->
+    match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
+      | [_,dir,_] ->
 	  if coq_path <> dir 
             (* If this is not the default -I . to coqtop *)
             && not
@@ -91,18 +91,54 @@ let add_load_path (phys_path,coq_path) =
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
 	      remove_load_path phys_path;
-	      load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+	      load_paths := (phys_path,coq_path,isroot) :: !load_paths;
 	    end
-      | _,[] ->
-	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+      | [] ->
+	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
-let load_paths_of_dir_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_paths)
-    
-let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
+let extend_path_with_dirpath p dir =
+  List.fold_left Filename.concat p 
+    (List.map string_of_id (List.rev (repr_dirpath dir)))
+
+let root_paths_matching_dir_path dir =
+  let rec aux = function
+  | [] -> []
+  | (p,d,true) :: l when is_dirpath_prefix_of d dir ->
+      let suffix = drop_dirpath_prefix d dir in
+      extend_path_with_dirpath p suffix :: aux l
+  | _ :: l -> aux l in
+  aux !load_paths
+
+(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
+(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
+
+(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
+(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *)
+
+let intersections d1 d2 =
+  let rec aux d1 =
+    if d1 = empty_dirpath then [d2] else
+      let rest = aux (snd (chop_dirpath 1 d1)) in
+      if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
+      else rest in
+  aux d1
+
+let loadpaths_matching_dir_path dir =
+  let rec aux = function
+  | [] -> []
+  | (p,d,true) :: l ->
+      let inters = intersections d dir in
+      List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl))
+	inters @
+	aux l
+  | (p,d,_) :: l ->
+      (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in
+  aux !load_paths
+
+let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
 
 (************************************************************************)
 (*s Modules on disk contain the following informations (after the magic 
@@ -197,6 +233,12 @@ let library_full_filename dir =
   try LibraryFilenameMap.find dir !libraries_filename_table
   with Not_found -> "<unavailable filename>"
 
+let overwrite_library_filenames f =
+  let f =
+    if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
+  LibraryMap.iter (fun dir _ -> register_library_filename dir f)
+    !libraries_table
+
 let library_is_loaded dir =
   try let _ = find_library dir in true
   with Not_found -> false
@@ -312,10 +354,8 @@ let (in_import, out_import) =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number = 08193 (* v8.2beta3 *)
-
 let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern vo_magic_number ".vo"
+  System.raw_extern_intern Coq_config.vo_magic_number ".vo"
 
 let with_magic_number_check f a =
   try f a
@@ -335,11 +375,11 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = load_paths_of_dir_path pref in
+  let loadpath = root_paths_matching_dir_path pref in
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = (string_of_id base)^".vo" in
-    let _, file = System.where_in_path loadpath name in
+    let _, file = System.where_in_path false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -348,20 +388,15 @@ let locate_absolute_library dir =
   else
     raise LibNotFound
 
-let locate_qualified_library qid =
+let locate_qualified_library warn qid =
   try
     (* Search library in loadpath *)
-    let dir, base = repr_qualid qid in 
-    let loadpath =
-      if repr_dirpath dir = [] then get_load_paths ()
-      else 
-        (* we assume dir is an absolute dirpath *)
-	load_paths_of_dir_path dir
-    in
+    let dir, base = repr_qualid qid in
+    let loadpath = loadpaths_matching_dir_path dir in
     if loadpath = [] then raise LibUnmappedDir;
-    let name =  (string_of_id base)^".vo" in
-    let path, file = System.where_in_path loadpath name in
-    let dir = extend_dirpath (find_logical_path path) base in
+    let name = string_of_id base ^ ".vo" in
+    let lpath, file = System.where_in_path warn (List.map fst loadpath) name in
+    let dir = extend_dirpath (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
     (* Otherwise, look for it in the file system *)
@@ -387,7 +422,7 @@ let try_locate_absolute_library dir =
 
 let try_locate_qualified_library (loc,qid) =
   try
-    let (_,dir,f) = locate_qualified_library qid in
+    let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
     dir,f
   with e -> 
     explain_locate_library_error qid e
@@ -590,8 +625,7 @@ let import_module export (loc,qid) =
 (*s Initializing the compilation of a library. *)
 
 let start_library f = 
-  let _,longf = 
-    System.find_file_in_path (get_load_paths ()) (f^".v") in
+  let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
@@ -609,9 +643,9 @@ let current_reexports () =
 
 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.")
+    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ 
+     strbrk " to save current library because" ++
+     strbrk " it already depends on a library of this name.")
 
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
diff --git a/library/library.mli b/library/library.mli
index 27ace544..a66a77bc 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: library.mli 8877 2006-05-30 16:37:04Z notin $ i*)
+(*i $Id: library.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list
   (* - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
+  (* - Overwrite the filename of all libraries (used when restoring a state) *)
+val overwrite_library_filenames : string -> unit
+
 (*s Hook for the xml exportation of libraries *)
 val set_xml_require : (dir_path -> unit) -> unit
 
@@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit
 
 val get_load_paths : unit -> System.physical_path list
 val get_full_load_paths : unit -> (System.physical_path * dir_path) list
-val add_load_path : System.physical_path * dir_path -> unit
+val add_load_path : bool -> System.physical_path * dir_path -> unit
 val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
 val is_in_load_paths : System.physical_path -> bool
-val load_paths_of_dir_path : dir_path -> System.physical_path list
 
 (*s Locate a library in the load paths *)
 exception LibUnmappedDir
@@ -73,7 +75,7 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  qualid -> library_location * dir_path * System.physical_path
+  bool -> qualid -> library_location * dir_path * System.physical_path
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/library/states.ml b/library/states.ml
index 169a3857..7f7fef47 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 9100 2006-08-31 18:04:26Z herbelin $ *)
+(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *)
 
 open System
 
@@ -19,12 +19,13 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let state_magic_number = 19764
-
 let (extern_state,intern_state) =
-  let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
+  let (raw_extern, raw_intern) =
+    extern_intern Coq_config.state_magic_number ".coq" in
   (fun s -> raw_extern s (freeze())),
-  (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s))
+  (fun s ->
+    unfreeze (raw_intern (Library.get_load_paths ()) s);
+    Library.overwrite_library_filenames s)
 
 (* Rollback. *)