diff options
| author | Hugo Herbelin | 2014-12-08 13:20:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-08 16:21:24 +0100 |
| commit | 5e331ad8920bcad2a749904aceebede9dfe7d1a7 (patch) | |
| tree | 5f80fcbe1b7b39b3562f242f2c522a9ee16945b7 /doc/RecTutorial/RecTutorial.v | |
| parent | 6b2c23ce5cfd7c0e25e835b5b3cc77909f60e2fe (diff) | |
This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.
As their commit messages suggested it, these commits were not intended
to be committed at this time. They are part of a on-going merge of the
code of induction and functional induction. Together with the fix
here, they are supposingly transparent, semantically speaking.
Diffstat (limited to 'doc/RecTutorial/RecTutorial.v')
0 files changed, 0 insertions, 0 deletions