diff options
| author | Pierre-Marie Pédrot | 2017-07-27 16:20:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-27 16:20:16 +0200 |
| commit | bc9a18bd48fb43a2aedd9c11df7a3e4244074120 (patch) | |
| tree | 831bfa310049e55666b6dbc79d50a3ca14cdb0ea /src | |
| parent | 6b3fd33d7e3b775ce6afe38f7b16d4b11bdccdb3 (diff) | |
Using thunks in the horrible Ltac2 example.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions