diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8c92329e5e..49690256c3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -773,6 +773,13 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "printing of existential variable instances"; + optkey = (TertiaryTable ("Printing","Existential","Instances")); + optread = (fun () -> !Constrextern.print_evar_arguments); + optwrite = (:=) Constrextern.print_evar_arguments } +let _ = + declare_bool_option + { optsync = true; optname = "implicit arguments printing"; optkey = (SecondaryTable ("Printing","Implicit")); optread = (fun () -> !Constrextern.print_implicits); @@ -870,7 +877,7 @@ let _ = declare_bool_option { optsync=true; optkey=SecondaryTable("Printing","Universes"); - optname="the printing of universes"; + optname="printing of universes"; optread=(fun () -> !Constrextern.print_universes); optwrite=(fun b -> Constrextern.print_universes:=b) } |