certains effets disparaissent a la sortie des sections, d'autres non (selon Summary.survive_section)

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

25 files changed, 74 insertions, 37 deletions

diff --git a/CHANGES b/CHANGES
index 250386151..a474a84c5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -74,6 +74,8 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
   Arguments" et non plus selon la valeur qu'elle avait au moment de la 
   définition dans la section.
 
+- SearchPattern / SearchRewrite (contrib de Yves Bertot)
+
 Tactiques
 
 - Langage de tactique
@@ -90,8 +92,6 @@ Tactiques
   en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
   source d'incompatibilité.
 
-- EAuto réussit parfois plus (source d'incompatibilité).
-
 - Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement
 
 - Plus de "Require Prolog" (intégré par défaut)
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 2901942ef..c04eee57e 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -370,6 +370,8 @@ Save.
 
 End Theory_of_rings.
 
+Hints Resolve Th_mult_zero_left Th_plus_reg_left : core.
+
 Implicit Arguments Off.
 
 Definition Semi_Ring_Theory_of :
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 7b96983a7..d2c379659 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -126,7 +126,8 @@ let _ =
   Summary.declare_summary "tactic-ring-table"
     { Summary.freeze_function = (fun () -> !theories_map);
       Summary.unfreeze_function = (fun t -> theories_map := t);
-      Summary.init_function = (fun () -> theories_map := Cmap.empty) }
+      Summary.init_function = (fun () -> theories_map := Cmap.empty);
+      Summary.survive_section = false }
 
 (* declare a new type of object in the environment, "tactic-ring-theory"
    The functions theory_to_obj and obj_to_theory do the conversions
diff --git a/library/declare.ml b/library/declare.ml
index b90dc2215..e1884ed5f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -52,7 +52,8 @@ let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
+	    Summary.init_function = (fun () -> vartab := Spmap.empty);
+	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,_,_) as vd)) =
   begin match d with (* Fails if not well-typed *)
@@ -114,7 +115,8 @@ let csttab = ref (Spmap.empty : strength Spmap.t)
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
+	    Summary.init_function = (fun () -> csttab := Spmap.empty);
+	    Summary.survive_section = false }
 
 let cache_constant (sp,(cdt,stre)) =
   begin match cdt with 
diff --git a/library/global.ml b/library/global.ml
index d5885ed02..2fcd3c2b6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -23,7 +23,8 @@ let _ =
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment) }
+      init_function = (fun () -> global_env := empty_environment);
+      survive_section = true }
 
 (* Then we export the functions of [Typing] on that environment. *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index dc5f994e3..59d0543e2 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -77,7 +77,8 @@ module MakeTable =
 	Summary.declare_summary kn
           { Summary.freeze_function = freeze;
             Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init }
+            Summary.init_function = init;
+	    Summary.survive_section = true }
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -219,7 +220,8 @@ let _ =
   Summary.declare_summary "Sync_option"
     { Summary.freeze_function = freeze_sync_table;
       Summary.unfreeze_function = unfreeze_sync_table;
-      Summary.init_function = init_sync_table }
+      Summary.init_function = init_sync_table;
+      Summary.survive_section = true }
 
 (* Tools for handling options *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 6ef403f59..3232c4848 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -314,7 +314,8 @@ let _ =
   Summary.declare_summary "implicits"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/lib.ml b/library/lib.ml
index a22f89353..9b5ba27b7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -9,7 +9,7 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string
+  | OpenedSection of string * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
   | ClosedSection of bool * string * library_segment * Nametab.module_contents
   | FrozenState of Summary.frozen
@@ -103,7 +103,7 @@ let contents_after = function
 
 let open_section s =
   let sp = make_path (id_of_string s) OBJ in
-  add_entry sp (OpenedSection s);
+  add_entry sp (OpenedSection (s, freeze_summaries()));
   path_prefix := !path_prefix @ [s];
   sp
 
@@ -138,10 +138,10 @@ let export_segment seg =
   clean [] seg
 
 let close_section export f s =
-  let sp = 
+  let sp,fs = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection s' -> 
-	  if s <> s' then error "this is not the last opened section"; sp
+      | sp,OpenedSection (s',fs) -> 
+	  if s <> s' then error "this is not the last opened section"; (sp,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
@@ -150,7 +150,7 @@ let close_section export f s =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  let contents = f sp after in
+  let contents = f fs sp after in
   add_entry (make_path (id_of_string s) OBJ)
     (ClosedSection (export, s,after',contents));
   Nametab.push_module s contents;
diff --git a/library/lib.mli b/library/lib.mli
index 96b1941ce..397e5a53b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -14,7 +14,7 @@ open Summary
 type node = 
   | Leaf of obj
   | Module of string
-  | OpenedSection of string
+  | OpenedSection of string * Summary.frozen
   | ClosedSection of bool * string * library_segment * Nametab.module_contents
   | FrozenState of Summary.frozen
 
@@ -41,8 +41,9 @@ val contents_after : section_path option -> library_segment
 
 val open_section : string -> section_path
 val close_section : export:bool ->
-  (section_path -> library_segment -> Nametab.module_contents) -> string
-    -> unit
+  (Summary.frozen -> section_path -> library_segment 
+     -> Nametab.module_contents) 
+  -> string -> unit
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
diff --git a/library/library.ml b/library/library.ml
index da7d01895..70cf895e5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -54,7 +54,8 @@ 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) }
+      Summary.init_function = (fun () -> modules_table := Stringmap.empty);
+      Summary.survive_section = true }
 
 let find_module s =
   try
diff --git a/library/nametab.ml b/library/nametab.ml
index c45e7d93e..de5c22c09 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -77,7 +77,8 @@ let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/summary.ml b/library/summary.ml
index 0ba07a737..8fbd5efe4 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -8,7 +8,8 @@ open Names
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit }
+  init_function : unit -> unit;
+  survive_section : bool }
 
 let summaries = 
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
@@ -21,7 +22,8 @@ let declare_summary sumname sdecl =
   let ddecl = {
     freeze_function = dyn_freeze;
     unfreeze_function = dyn_unfreeze;
-    init_function = dyn_init} 
+    init_function = dyn_init;
+    survive_section = sdecl.survive_section } 
   in
   if Hashtbl.mem summaries sumname then
     anomalylabstrm "Summary.declare_summary"
@@ -44,5 +46,14 @@ let unfreeze_summaries fs =
        with Not_found -> decl.init_function())
     summaries
 
+let unfreeze_lost_summaries fs =
+  Hashtbl.iter
+    (fun id decl -> 
+       try 
+	 if not decl.survive_section then
+	   decl.unfreeze_function (Stringmap.find id fs)
+       with Not_found -> decl.init_function())
+    summaries
+
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
index 0d329a947..fc639d7f8 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,7 +11,8 @@ open Names
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit }
+  init_function : unit -> unit;
+  survive_section : bool }
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
@@ -19,6 +20,7 @@ type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
+val unfreeze_lost_summaries : frozen -> unit
 val init_summaries : unit -> unit
 
 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 7c4c40aa1..1d1deed7d 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -248,7 +248,7 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (_,Lib.OpenedSection str) -> 
+    | (_,Lib.OpenedSection (str,_)) -> 
         [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
     | (sp,Lib.ClosedSection _) -> 
         [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
@@ -286,7 +286,7 @@ let list_filter_vec f vec =
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection str) as hd)::rest ->
+    | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
         if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a452cf645..89542564d 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -182,7 +182,8 @@ let _ =
   Summary.declare_summary "inh_graph"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 (* classe d'un terme *)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 45b16c935..ef0e839bb 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -104,4 +104,5 @@ let _ =
   Summary.declare_summary "objdefs"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index f90627f7e..4801d017e 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -14,7 +14,8 @@ let _ = Summary.declare_summary
 	  "SYNTAXCONSTANT"
 	  { Summary.freeze_function = (fun () -> !syntax_table);
 	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := Spmap.empty) }
+	    Summary.init_function = (fun () -> syntax_table := Spmap.empty);
+	    Summary.survive_section = false }
 
 let add_syntax_constant sp c =
   syntax_table := Spmap.add sp c !syntax_table
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1edeb78f8..ca2bcb705 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -49,7 +49,8 @@ let _ =
   Summary.declare_summary "evaluation"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 
 (* Check that c is an "elimination constant"
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 422d41222..4cd1641b1 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -169,7 +169,8 @@ let _ =
   Summary.declare_summary "tactic-definition"
     { Summary.freeze_function   = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
+      Summary.init_function     = init;
+      Summary.survive_section   = false }
 
 (* Unboxes the tactic_arg *)
 let unvarg = function
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 27b04eedb..70ff2e639 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -142,7 +142,8 @@ let unfreeze fs = searchtable := fs
 let _ = Summary.declare_summary "search"
 	  { Summary.freeze_function   = freeze;
 	    Summary.unfreeze_function = unfreeze;
-	    Summary.init_function     = init }
+	    Summary.init_function     = init;
+	    Summary.survive_section   = false }
 
  
 (**************************************************************************)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 628c337f9..6497287ab 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -177,7 +177,8 @@ let _ =
   Summary.declare_summary "destruct-hyp-concl"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = true }
 
 let cache_dd (_,(na,dd)) =
   try 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a90114641..96c323d73 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1574,7 +1574,8 @@ let _ =
   Summary.declare_summary "autorewrite"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = init;
+      Summary.survive_section = false }
 
 (*Adds a list of rules to the rule table*)
 let add_list_rules rbase lrl = 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6e79134bb..2b552fffc 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -290,13 +290,14 @@ and module_contents seg =
 
 let close_section _ s = 
   let oldenv = Global.env() in
-  let process_segment sec_sp decls =
+  let process_segment fs sec_sp decls =
     let newdir = dirpath sec_sp in
     let olddir = wd_of_sp sec_sp in
     let (ops,ids,_) = 
       List.fold_left 
 	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
     in 
+    Summary.unfreeze_lost_summaries fs;
     Global.pop_named_decls ids;
     List.iter process_operation (List.rev ops);
     module_contents decls 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index eb7543f3d..0597238cd 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -38,7 +38,8 @@ let _ =
   declare_summary "syntax"
     { freeze_function = Esyntax.freeze;
       unfreeze_function = Esyntax.unfreeze;
-      init_function = Esyntax.init }
+      init_function = Esyntax.init;
+      survive_section = false }
 
 (* Pretty-printing objects = syntax_entry *)
 let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj
@@ -69,7 +70,8 @@ let _ =
   declare_summary "GRAMMAR_LEXER"
     { freeze_function = Egrammar.freeze;
       unfreeze_function = Egrammar.unfreeze;
-      init_function = Egrammar.init}
+      init_function = Egrammar.init;
+      survive_section = false }
 
 (* Tokens *)
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index f255739b3..0c81359cb 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -200,7 +200,8 @@ let _ =
   Summary.declare_summary "ML-MODULES"
     { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
       Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
-      Summary.init_function = (fun () -> init_ml_modules ()) }
+      Summary.init_function = (fun () -> init_ml_modules ());
+      Summary.survive_section = true }
 
 (* Same as restore_ml_modules, but verbosely *)