bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo plus petits

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

7 files changed, 27 insertions, 20 deletions

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 3ff4f51f46..4b5fff53dc 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -228,8 +228,6 @@ Save.
 
 Hints Resolve Th_plus_permute Th_mult_permute.
 
-Lemma Th_mult_zero_left :(n:A)[| 0*n == 0 |].
-
 Lemma aux1 : (a:A) [| a + a == a |] -> [| a == 0 |].
 Intros.
 Generalize (opp_def a).
@@ -242,6 +240,7 @@ Rewrite plus_zero_left.
 Trivial.
 Save.
 
+Lemma Th_mult_zero_left :(n:A)[| 0*n == 0 |].
 Intros.
 Apply aux1.
 Rewrite <- distr_left.
@@ -253,7 +252,6 @@ Hints Resolve Th_mult_zero_left.
 Lemma Th_mult_zero_left2 : (n:A)[| 0 == 0*n |].
 Symmetry; EAuto. Save.
 
-Lemma Th_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |].
 Lemma aux2 : (x,y,z:A) [|x+y==0|] -> [|x+z==0|] -> y==z.
 Intros.
 Rewrite <- (plus_zero_left y).
@@ -266,6 +264,7 @@ Rewrite plus_zero_left.
 Reflexivity.
 Save.
 
+Lemma Th_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |].
 Intros.
 Apply (aux2 1![|x*y|]);
 [ Apply opp_def
@@ -314,7 +313,7 @@ Lemma Th_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |].
 Intros.
 Apply (aux2 1![| x + y |]);
 [ Elim plus_assoc;
-  Rewrite -> (Th_plus_permute y [|-x|]); Rewrite -> plus_assoc;
+  Rewrite -> (Th_plus_permute y [| -x |]); Rewrite -> plus_assoc;
   Rewrite -> opp_def;  Rewrite plus_zero_left; Auto
 | Auto ].
 Save.
@@ -322,8 +321,8 @@ Save.
 Lemma Th_plus_permute_opp: (n,m,p:A)[| (-m) + (n + p) == n + ((-m)+p) |].
 EAuto. Save.
 
-Lemma Th_opp_opp : (n:A)[|-(-n) == n |].
-Intro; Apply (aux2 1![|-n|]); 
+Lemma Th_opp_opp : (n:A)[| -(-n) == n |].
+Intro; Apply (aux2 1![| -n |]); 
   [ Auto | Elim plus_sym; Auto ].
 Save.
 Hints Resolve Th_opp_opp.
@@ -345,7 +344,7 @@ Auto. Save.
 Lemma Th_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p.
 Intros; Generalize (congr_eqT ? ? [z][| (-n)+z |] ? ? H).
 Repeat Rewrite plus_assoc.
-Rewrite (plus_sym [|-n|] n).
+Rewrite (plus_sym [| -n |] n).
 Rewrite opp_def.
 Repeat Rewrite Th_plus_zero_left; EAuto.
 Save.
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
index 38572b7207..4d8e3092ac 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -29,6 +29,7 @@ case $coqdebug in
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev \
+        -I $COQTOP/contrib/omega -I $COQTOP/contrib/ring \
 	$* $args;;
     *) exec $OCAMLDEBUG $*;;
 esac
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index eab3cb0e48..93a84c7c7b 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -32,7 +32,7 @@ val cook_constant : constant_value -> constr
 
 (*s Constant declaration. *)
 
-type constant_entry= {
+type constant_entry = {
   const_entry_body : lazy_constant_value;
   const_entry_type : constr option }
 
diff --git a/lib/system.ml b/lib/system.ml
index aed203b206..605cbca875 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -99,7 +99,7 @@ let open_trapping_failure open_fun name suffix =
 let try_remove f =
   try Sys.remove f
   with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
-                     'sTR f ; 'sTR" which is corrupted !!" >]
+                     'sTR f ; 'sTR" which is corrupted!" >]
 
 let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures]
 let marshal_in ch = Marshal.from_channel ch
diff --git a/library/lib.ml b/library/lib.ml
index 8d91666a38..387bf41f19 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -122,6 +122,11 @@ let start_module s =
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
+let rec clean_segment = function
+  | [] -> []
+  | (_,FrozenState _) :: l -> clean_segment l
+  | node :: l -> node :: (clean_segment l)
+
 let close_section s =
   let sp = 
     try match find_entry_p is_opened_section with
@@ -133,9 +138,10 @@ let close_section s =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry (make_path (id_of_string s) OBJ) (ClosedSection (s,after));
+  let after' = clean_segment after in
+  add_entry (make_path (id_of_string s) OBJ) (ClosedSection (s,after'));
   pop_path_prefix ();
-  (sp,after)
+  (sp,after')
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
@@ -143,16 +149,15 @@ let close_section s =
 
 let export_module () =
   if !module_name = None then error "no module declared";
-  let rec export acc = function
+  let rec clean acc = function
     | (_,Module _) :: _ -> acc
-    | (_,Leaf _) as node :: stk -> export (node::acc) stk
-    | (_,ClosedSection _) as node :: stk -> export (node::acc) stk
+    | (_,Leaf _) as node :: stk -> clean (node::acc) stk
+    | (_,ClosedSection _) as node :: stk -> clean (node::acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
-    | (_,FrozenState _) :: stk -> export acc stk
+    | (_,FrozenState _) :: stk -> clean acc stk
     | _ -> assert false
   in
-  export [] !lib_stk
-
+  clean [] !lib_stk
 
 (* Backtracking. *)
 
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index 76b993b218..c03334aebd 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -14,7 +14,7 @@
 (****************************************************************************)
 
 Grammar tactic simple_tactic :=
-  eapply [ "EApply" com_binding_list($cl) ]
+  eapply [ "EApply" constrarg_binding_list($cl) ]
       -> [(EApplyWithBindings ($LIST $cl))]
 | eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
 | prolog [ "Prolog" "[" constrarg_list($l) "]" numarg($n) ]
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 820100f6fc..da223b541a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -190,12 +190,14 @@ let expmod_constant_value opaque oldenv modlist = function
   | None -> None
   | Some { contents = Cooked c } -> 
       if opaque then 
-	Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
+	(* None *)
+        Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
       else
 	Some (ref (Cooked (expmod_constr oldenv modlist c)))
   | Some { contents = Recipe f } -> 
       Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ()))))
 
+
 (* Discharge of inductive types. *)
 
 let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
@@ -324,7 +326,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
     | "STRUCTURE" ->
 	let ((sp,i),info) = outStruc lobj in
 	let newsp = recalc_sp sp in
-	let mib = Environ.lookup_mind newsp oldenv in
+	let mib = Environ.lookup_mind sp oldenv in
 	let strobj =
 	  { s_CONST = info.s_CONST;
 	    s_PARAM = mib.mind_nparams;