diff options
| author | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
| commit | 8bd60579d4768793c849b9b4cd46f14d33d0f71d (patch) | |
| tree | 9fb0510584dae4f5416f8776b26cd7964ceb810f /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | e3e8dfb4c2f30ed1c6715999e1f74914e7bc187b (diff) | |
| parent | feb9c50b5812a01e9dc60e2408f4f9f38986ce8c (diff) | |
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions