diff options
| author | Pierre-Marie Pédrot | 2020-09-02 20:33:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-04 14:04:48 +0200 |
| commit | 06d6dda7872607754423a5ec43e488ad59e13b18 (patch) | |
| tree | 112685855c6d5d2a00c7916c13d2a37ee854db62 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 2000ba38718e72133b258b378b118a495acb6ffc (diff) | |
Enforce the argument of elim functions to be a variable.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions