diff options
| author | Hugo Herbelin | 2016-07-19 10:44:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-19 11:45:48 +0200 |
| commit | b663b735adaf546192ff5b25b608dda55e05f3d8 (patch) | |
| tree | 1e9c391964bd85dcd03b4ac209a91989b6a4a5ad /kernel/type_errors.ml | |
| parent | b3e7ef09210267e6d34bc1ac377e66c7fec7e739 (diff) | |
Notations with multiple recursive binders: fixing use of alpha-conversion.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions