diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 14:23:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:48 +0200 |
| commit | 8c74d3e5578caeb5c62ba462528d9972c1de17f1 (patch) | |
| tree | d85d73110a1eb95b8873375cee0bd35821996657 /theories/MSets | |
| parent | df1e24f64f68318221d08246098837368ee1b406 (diff) | |
Passing around the precedence to the generic printer so as to solve
the remaining issue with the fix to #3709.
However, this does not solve the problem in mind which is that
"intuition idtac; idtac" is printed with extra parentheses into
"intuition (idtac; idtac)".
If one change the level of printing of TacArg of Tacexp from latom to
inherited, this breaks elsewhere, with "let x := (simpl) in idtac"
printed "let x := simpl in idtac".
Diffstat (limited to 'theories/MSets')
0 files changed, 0 insertions, 0 deletions