diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 22:21:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 22:21:29 +0000 |
| commit | db49598f897eec7482e2c26a311f77a52201416e (patch) | |
| tree | 91bcd60b9687f2f94f057bf82b8fdf9dbe0dc08f /contrib | |
| parent | 145ad94fc96a4989c24061de7a90b7520d530932 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun_common.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 78e2c4408..4010b49d5 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 |