diff options
| author | Hugo Herbelin | 2016-04-09 11:56:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:25:59 +0200 |
| commit | ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 (patch) | |
| tree | 70cd706240e86e9ecf3fe3ce1f99eee6f896381a /kernel | |
| parent | bb43730ac876b8de79967090afa50f00858af6d5 (diff) | |
In pr_clauses, do not print a leading space by default so that it can
be used in the generic printer for tactics.
Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions