aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-06-22 14:21:43 +0200
committerGaëtan Gilbert2017-08-01 19:28:11 +0200
commite18f0a289411047777efdfa362bba675b16bb5a3 (patch)
tree77a5a655d1dfa3a87ede6e7247bfd4215442b168 /dev/doc
parentfc4c6c604db7bd6d973b02d29993daafeabc6f6c (diff)
Unbreak RecTutorial.v
The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions