diff options
| author | Maxime Dénès | 2019-09-02 11:45:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-02 11:45:45 +0200 |
| commit | de164747a3296f693a2ac9bb11c1778b487a50c4 (patch) | |
| tree | db52364e58f56d483e514d04f4c159d73fd7debe /kernel/type_errors.ml | |
| parent | 9402c94c64e08367de1523fd72f6705691ba04d3 (diff) | |
| parent | bfe93b7c7b737ae2b1ccb52ffc05a5b241cc9c20 (diff) | |
Merge PR #10562: [library] Move library to vernac
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions