diff options
| author | Enrico Tassi | 2019-03-21 10:08:29 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:44 +0200 |
| commit | e68bccba9344c1b3d77d3e815af6cce1ce50b731 (patch) | |
| tree | b155f20564f0bd20bc15184f943d4b4501e2a770 /doc/plugin_tutorial/tuto1/src/simple_print.ml | |
| parent | 600fef9a1c9cd15ad43196b7750ba15922c01752 (diff) | |
[ssr] new syntax for the under tactic
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_print.ml')
0 files changed, 0 insertions, 0 deletions