diff options
| author | Hugo Herbelin | 2020-11-29 02:10:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2021-01-18 15:42:00 +0100 |
| commit | 53e287871e2d03f95e754ffa58047668799e54ee (patch) | |
| tree | 9e8b87861394d86d43a06d803212d15c93b4b0a3 /pretyping/typeclasses_errors.ml | |
| parent | 861c22919da6877b91ed5a095e6b0e95725ca225 (diff) | |
Further simplifications in intro_patterns machinery.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions