diff options
| author | Andreas Lynge | 2019-07-01 12:57:36 +0200 |
|---|---|---|
| committer | Andreas Lynge | 2019-08-10 03:22:55 +0200 |
| commit | 167d062c47f389340d5c50d022571524b2746a51 (patch) | |
| tree | 580d9d0b3571aa5cf753cf74a6fc4721841afb78 /doc/plugin_tutorial/tuto2/src/persistent_counter.ml | |
| parent | b8477fb38842016c226ba9d7be8f60486411a2ee (diff) | |
Make rewrite use the registered elimination schemes
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/persistent_counter.ml')
0 files changed, 0 insertions, 0 deletions