diff options
| author | Pierre-Marie Pédrot | 2015-10-02 16:27:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-02 16:33:15 +0200 |
| commit | 944c8de0bfe4048e0733a487e6388db4dfc9075a (patch) | |
| tree | af037ad2d990da53529356fec44860ad9ca87577 /plugins/funind/indfun_common.ml | |
| parent | 16c88c9be5c37ee2e4fe04f7342365964031e7dd (diff) | |
| parent | 8860362de4a26286b0cb20cf4e02edc5209bdbd1 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1c409500ef..35bd1c36da 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -180,9 +180,10 @@ let get_proof_clean do_reduce = let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () - and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () - in + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in + let old_printuniverses = !Constrextern.print_universes in + Constrextern.print_universes := true; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -195,6 +196,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; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); res with @@ -203,6 +205,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; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); raise reraise |