diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-22 13:52:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-01 19:28:11 +0200 |
| commit | fc4c6c604db7bd6d973b02d29993daafeabc6f6c (patch) | |
| tree | a96d0cad0c47a39c69473b98ab581f9d3992196b /pretyping/indrec.ml | |
| parent | 8d85f0876d28a760bca693624f98145e4ee8f331 (diff) | |
Remove old doc/rt files.
Diffstat (limited to 'pretyping/indrec.ml')
0 files changed, 0 insertions, 0 deletions