diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 142978009a2585a1af82b3081720d680028c2108 (patch) | |
| tree | 20d46dbf2b45bfad53af2a9873839cd4d67befab /doc/tutorial/Tutorial.tex | |
| parent | 82b97b07fc56dbe03109e2f38f50849dce1d69d5 (diff) | |
Revert "Simplification in ppvernac.ml."
This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
0 files changed, 0 insertions, 0 deletions