diff options
| author | Pierre Courtieu | 2016-01-06 17:24:28 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2016-01-06 17:24:28 +0100 |
| commit | 4558ea05882f4b207d1de0224a04aa995d423701 (patch) | |
| tree | ab3326e0ddf181a86f0dbfeb7a3ea60ee3cc69d1 /pgshell | |
| parent | a326ff399be1691643fe4bbbde4a27896b194e82 (diff) | |
Adding uset preference coq-indent-semicolon-tactical.
Some people prefer ";" tactical to be non indented, in particular in
Ltac definitions. Setting this variable to 0 (2 by default) does it. You
can still have some indentation by putting ; at beginning of lines:
tac1
; tac2
; tac3.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions