diff options
| author | Pierre-Marie Pédrot | 2015-01-28 20:12:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-28 20:12:42 +0100 |
| commit | 2947dd269744bcb9b0a487e262e8f21bb2a382eb (patch) | |
| tree | 298e2159dd7b4e7ff40ef9c1ea0a764fc5e0a852 /pretyping/typeclasses_errors.mli | |
| parent | 0ff6b07d67560dc46b8becf4780ce1283cbece4e (diff) | |
Fixing bug #3931.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions