diff options
| author | Maxime Dénès | 2018-12-21 18:01:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-22 11:11:34 +0100 |
| commit | 4922d0d6e156338485b48ce3fd34c1179a505083 (patch) | |
| tree | 2562bb8e677ff9afb7d51a8a079ce282c2b844da /pretyping/typeclasses_errors.ml | |
| parent | b6ac490a583c83096d810c25e89d01fb7d25741f (diff) | |
VernacDeclareClass -> VernacExistingClass
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions