diff options
| author | Hugo Herbelin | 2017-07-08 17:12:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 74dfaaa8555f53bfc75216205823a8020e80b6a1 (patch) | |
| tree | 30676a703026d34224174087a98285ff62a0156f /dev/doc | |
| parent | 93a65415ff582d2ceb5bb9d994edaa6068da8280 (diff) | |
Selecting which notation to print based on current stack of scope.
See discussion on coq-club starting on 23 August 2016.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions