diff options
| author | Abhishek Anand (optiplex7010@home) | 2020-02-20 19:52:39 -0800 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-23 18:05:00 +0100 |
| commit | 38c47ac0626fed51d17bc7513d7dbbd63053016e (patch) | |
| tree | 995ead018d1c30343b925ea45a8ffa3bb5124845 /vernac | |
| parent | 0dc4b008c753fa4e20ea95630edea9e3e32c68c0 (diff) | |
added the new option
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63fc587f71..cd8e699066 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1282,6 +1282,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Parens"]; + optread = (fun () -> !Constrextern.print_parens); + optwrite = (fun b -> Constrextern.print_parens := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } |