gros commit de tout ce que j'ai fait pendant les vacances :

 - tactics/Equality
 - debug du discharge
 - constr_of_compattern implante vite fait / mal fait en attendant mieux
 - theories/Logic (ne passe pas entierrement)


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

6 files changed, 41 insertions, 33 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ff46ad72ae..5e87c1a749 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,12 +57,11 @@ let cache_variable (sp,(id,(ty,_,_) as vd,imps)) =
   if imps then declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
 
-let load_variable _ = anomaly "we shouldn't load a variable"
+let load_variable _ = ()
 
-let open_variable _ = anomaly "we shouldn't open a variable"
+let open_variable _ = ()
 
-let specification_variable _ = 
-  anomaly "we shouldn't extract the specification of a variable"
+let specification_variable x = x
 
 let (in_variable, out_variable) =
   let od = {
diff --git a/library/global.ml b/library/global.ml
index af9dbe1d5b..9242672883 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -37,6 +37,8 @@ let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
+let pop_vars ids = global_env := pop_vars ids !global_env
+
 let lookup_var id = lookup_var id !global_env
 let lookup_rel n = lookup_rel n !global_env
 let lookup_constant sp = lookup_constant sp !global_env
diff --git a/library/global.mli b/library/global.mli
index e9e42cf5eb..fbf0345277 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -30,6 +30,8 @@ val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
 val add_constraints : constraints -> unit
 
+val pop_vars : identifier list -> unit
+
 val lookup_var : identifier -> name * typed_type
 val lookup_rel : int -> name * typed_type
 val lookup_constant : section_path -> constant_body
diff --git a/library/lib.ml b/library/lib.ml
index 75caa48167..8d91666a38 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -9,7 +9,8 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string * Summary.frozen
+  | OpenedSection of string
+  | ClosedSection of string * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -101,8 +102,7 @@ let contents_after = function
 
 let open_section s =
   let sp = make_path (id_of_string s) OBJ in
-  let fs = freeze_summaries () in
-  add_entry sp (OpenedSection (s,fs));
+  add_entry sp (OpenedSection s);
   path_prefix := !path_prefix @ [s];
   sp
 
@@ -123,18 +123,19 @@ let start_module s =
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
 let close_section s =
-  let (sp,frozen) = 
+  let sp = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection (s',fs) -> 
-	  if s <> s' then error "this is not the last opened section"; (sp,fs)
+      | sp,OpenedSection s' -> 
+	  if s <> s' then error "this is not the last opened section"; sp
       | _ -> assert false
     with Not_found ->
       error "no opened section"
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
+  add_entry (make_path (id_of_string s) OBJ) (ClosedSection (s,after));
   pop_path_prefix ();
-  (sp,after,frozen)
+  (sp,after)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
@@ -145,6 +146,7 @@ let export_module () =
   let rec export acc = function
     | (_,Module _) :: _ -> acc
     | (_,Leaf _) as node :: stk -> export (node::acc) stk
+    | (_,ClosedSection _) as node :: stk -> export (node::acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,FrozenState _) :: stk -> export acc stk
     | _ -> assert false
diff --git a/library/lib.mli b/library/lib.mli
index 36b49bbeb2..1d601f7b60 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -14,7 +14,8 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string * Summary.frozen
+  | OpenedSection of string
+  | ClosedSection of string * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -34,7 +35,7 @@ val contents_after : section_path option -> library_segment
 (*s Opening and closing a section. *)
 
 val open_section : string -> section_path
-val close_section : string -> section_path * library_segment * Summary.frozen
+val close_section : string -> section_path * library_segment
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
diff --git a/library/library.ml b/library/library.ml
index 913f396d94..893a449212 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -29,30 +29,31 @@ type module_t = {
   module_deps : (string * Digest.t * bool) list;
   module_digest : Digest.t }
 
-let modules_table =
-  (Hashtbl.create 17 : (string, module_t) Hashtbl.t)
+let modules_table = ref Stringmap.empty
+
+let _ = 
+  Summary.declare_summary "MODULES"
+    { Summary.freeze_function = (fun () -> !modules_table);
+      Summary.unfreeze_function = (fun ft -> modules_table := ft);
+      Summary.init_function = (fun () -> modules_table := Stringmap.empty) }
 
 let find_module s =
   try
-    Hashtbl.find modules_table s
+    Stringmap.find s !modules_table
   with Not_found ->
     error ("Unknown module " ^ s)
 
 let module_is_loaded s =
-  try let _ = Hashtbl.find modules_table s in true with Not_found -> false
+  try let _ = Stringmap.find s !modules_table in true with Not_found -> false
 
-let module_is_opened s =
-  (find_module s).module_opened
+let module_is_opened s = (find_module s).module_opened
 
 let loaded_modules () =
-  let l = ref [] in
-  Hashtbl.iter (fun s _ -> l := s :: !l) modules_table;
-  !l
+  Stringmap.fold (fun s _ l -> s :: l) !modules_table []
 
 let opened_modules () =
-  let l = ref [] in
-  Hashtbl.iter (fun s m -> if m.module_opened then l := s :: !l) modules_table;
-  !l
+  Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l) 
+    !modules_table []
 
 let vo_magic_number = 0700
 
@@ -63,6 +64,7 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
+    | _,ClosedSection (_,seg) -> iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
@@ -106,7 +108,7 @@ let rec load_module_from doexp s f =
   List.iter (load_mandatory_module doexp s) m.module_deps;
   Global.import m.module_compiled_env;
   load_objects m.module_declarations;
-  Hashtbl.add modules_table s m;
+  modules_table := Stringmap.add s m !modules_table;
   m
 
 and load_mandatory_module doexp caller (s,d,export) =
@@ -116,8 +118,10 @@ and load_mandatory_module doexp caller (s,d,export) =
   if doexp && export then open_module s
 
 and find_module doexp s f =
-  try Hashtbl.find modules_table s with Not_found -> load_module_from doexp s f
-
+  try 
+    Stringmap.find s !modules_table 
+  with Not_found -> 
+    load_module_from doexp s f
 
 let load_module s = function
   | None -> let _ = load_module_from true s s in ()
@@ -138,11 +142,9 @@ let require_module spec name fileopt export =
 (* [save_module s] saves the module [m] to the disk. *)
 
 let current_imports () =
-  let l = ref [] in
-  Hashtbl.iter 
-    (fun _ m -> l := (m.module_name, m.module_digest, m.module_exported) :: !l)
-    modules_table;
-  !l
+  Stringmap.fold
+    (fun _ m l -> (m.module_name, m.module_digest, m.module_exported) :: l)
+    !modules_table []
 
 let save_module_to s f =
   let seg = export_module () in