diff options
| author | Gaëtan Gilbert | 2020-02-06 14:17:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 16:23:49 +0100 |
| commit | e1f24fc75514d9720205259cf6a25b5b92e6a976 (patch) | |
| tree | 1185647ff466ff18046eb8640f8ed419fcfedf06 /pretyping/program.ml | |
| parent | 4563779bf990cf22d88474a68acf4eb9cfd8d173 (diff) | |
overlay for removal of optname
Diffstat (limited to 'pretyping/program.ml')
0 files changed, 0 insertions, 0 deletions