From d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 18 Jul 2008 15:58:12 +0000
Subject: 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
---
 contrib/funind/indfun_common.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'contrib/funind')

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
 
 
-- 
cgit v1.2.3