diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cb1f21149f..81bcd47352 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -760,8 +760,16 @@ let _ = { optsync = true; optname = "coercion printing"; optkey = (SecondaryTable ("Printing","Coercions")); - optread = (fun () -> !Termast.print_coercions); - optwrite = (fun b -> Termast.print_coercions := b) } + optread = (fun () -> !Constrextern.print_coercions); + optwrite = (fun b -> Constrextern.print_coercions := b) } + +let _ = + declare_bool_option + { optsync = true; + optname = "implicits printing"; + optkey = (SecondaryTable ("Printing","Implicits")); + optread = (fun () -> !Constrextern.print_implicits); + optwrite = (fun b -> Constrextern.print_implicits := b) } let _ = declare_bool_option |