From db49598f897eec7482e2c26a311f77a52201416e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Apr 2008 22:21:29 +0000
Subject: Désactivation du dumping des notations quand funind appelle les
 commandes d'interprétation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10784 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/indfun_common.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 78e2c44087..4010b49d56 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -238,16 +238,20 @@ 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;
   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;
     res
   with  
     | e -> 
@@ -255,6 +259,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;
 	raise e
 
 
-- 
cgit v1.2.3