Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from de coqdoc (compatibilité)

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

2 files changed, 10 insertions, 10 deletions

diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 4010b49d56..a3c169b7ec 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -238,20 +238,19 @@ let with_full_print f a =
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in 
-  let old_dump = !Flags.dump in 
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
   Impargs.make_contextual_implicit_args false;
   Impargs.make_contextual_implicit_args false;
-  Flags.dump := false;
+  Dumpglob.pause ();
   try 
     let res = f a in 
     Impargs.make_implicit_args old_implicit_args;
     Impargs.make_strict_implicit_args old_strict_implicit_args;
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
-    Flags.dump := old_dump;
+    Dumpglob.continue ();
     res
   with  
     | e -> 
@@ -259,7 +258,7 @@ let with_full_print f a =
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
-	Flags.dump := old_dump;
+	Dumpglob.continue ();
 	raise e
 
 
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 71aa7e99ee..fbb4589b8e 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -120,7 +120,7 @@ let dump_variable lid = ()
 let vernac_assumption env isevars kind l nl =
   let global = fst kind = Global in
     List.iter (fun (is_coe,(idl,c)) -> 
-      if !Flags.dump then
+      if Dumpglob.dump () then
 	List.iter (fun lid -> 
 	  if global then dump_definition lid "ax" 
 	  else dump_variable lid) idl;
@@ -140,7 +140,7 @@ let subtac (loc, command) =
   match command with
   | VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
       check_fresh lid;
-      dump_definition lid "def";
+      if Dumpglob.dump () then dump_definition lid "def";
       (match expr with
       | ProveBody (bl, t) -> 
 	  if Lib.is_modtype () then
@@ -153,12 +153,12 @@ let subtac (loc, command) =
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
-	dump_definition lid "fix") l;
+	if Dumpglob.dump () then dump_definition lid "fix") l;
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l b)
 	  
   | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
-      if !Flags.dump then dump_definition id "prf";
+      if Dumpglob.dump () then dump_definition id "prf";
       if not(Pfedit.refining ()) then
 	if lettop then
 	  errorlabstrm "Subtac_command.StartProof"
@@ -173,11 +173,12 @@ let subtac (loc, command) =
       vernac_assumption env isevars stre l nl
 	
   | VernacInstance (glob, sup, is, props, pri) ->
-      if !Flags.dump then dump_constraint "inst" is;
+      if Dumpglob.dump () then dump_constraint "inst" is;
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 	
   | VernacCoFixpoint (l, b) ->
-      List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
+      if Dumpglob.dump () then 
+	List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
       ignore(Subtac_command.build_corecursive l b)
 	
   (*| VernacEndProof e ->