diff options
| author | Emilio Jesus Gallego Arias | 2020-02-20 13:56:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-20 13:56:23 -0500 |
| commit | f748ca04748ef00b85de7f31dc1dc7f0a985ec3f (patch) | |
| tree | 60a101df6b546e33878a9ac0900d1009f666c7be /printing/printer.ml | |
| parent | 935101ee1375ed930e993d0e76f2325ade562506 (diff) | |
| parent | a8307ceecc4347593e67cff2044a250b75060f5a (diff) | |
Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions