aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
authorAbhishek Anand (optiplex7010@home)2020-02-22 13:22:27 -0800
committerHugo Herbelin2020-02-23 18:05:32 +0100
commit5820b274acda8be0372471758842b0ea2b950d41 (patch)
tree272a8c54fa449ff44c8bba215f4c021d5234d405 /vernac
parentdd5a748cbec3abd9a11bbdd3ed4c14497b575fb9 (diff)
parens --> parentheses
Diffstat (limited to 'vernac')
-rw-r--r--vernac/vernacentries.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cd8e699066..2eb1aa39b0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1282,9 +1282,9 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optkey = ["Printing";"Parens"];
- optread = (fun () -> !Constrextern.print_parens);
- optwrite = (fun b -> Constrextern.print_parens := b) }
+ optkey = ["Printing";"Parentheses"];
+ optread = (fun () -> !Constrextern.print_parentheses);
+ optwrite = (fun b -> Constrextern.print_parentheses := b) }
let () =
declare_bool_option