diff options
| author | Hugo Herbelin | 2016-07-17 09:34:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 09:37:53 +0200 |
| commit | d17237cfd3a67b9a93de98a23ae29869456d2028 (patch) | |
| tree | 5a323cfed9cee00a8dc23b1fac710bbe408c23aa /kernel/type_errors.ml | |
| parent | 91f44b164c5d9fa170a8faa7227aff08c1335861 (diff) | |
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions