diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-22 14:21:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-01 19:28:11 +0200 |
| commit | e18f0a289411047777efdfa362bba675b16bb5a3 (patch) | |
| tree | 77a5a655d1dfa3a87ede6e7247bfd4215442b168 /proofs/redexpr.ml | |
| parent | fc4c6c604db7bd6d973b02d29993daafeabc6f6c (diff) | |
Unbreak RecTutorial.v
The RecTutorial.tex still contains similarly broken Coq code, it just
doesn't run it.
Diffstat (limited to 'proofs/redexpr.ml')
0 files changed, 0 insertions, 0 deletions