diff options
| author | Pierre-Marie Pédrot | 2020-12-31 15:59:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-31 15:59:39 +0100 |
| commit | f26f263250f0bd2ded25d16d1c6a650b92f7f63b (patch) | |
| tree | 80ba6fcb8b6b1a43319259b3a06da223917bc1fd /kernel/nativecode.mli | |
| parent | 8719fb545724b020808e2d1f8443495297d62ea5 (diff) | |
Adding a test for conversion involving let-bindings in inductive parameters.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions