diff options
| author | Hugo Herbelin | 2014-12-07 17:59:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-14 13:12:01 +0100 |
| commit | c7a7d55e0dc47a097bf0d0c8897bc490ce55577b (patch) | |
| tree | d1305711dd507b512ba97f0c57b85cabcbff1579 /dev | |
| parent | 8e06c02845df0f1243ca260c7707cc912734c704 (diff) | |
Update in the documentation of parts of the code of destruct/induction.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions