diff options
| author | Arnaud Spiwack | 2014-07-22 17:55:00 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-23 17:52:46 +0200 |
| commit | 7e577f93aca95d10584014e1d88dfbf314b74f9f (patch) | |
| tree | dc4bc5197a1085098c756b76bc8b0c5356f38b00 /kernel/type_errors.ml | |
| parent | e143cffaeab1a294ca08a49443747c66bc963c29 (diff) | |
Derive plugin: a more general interface.
Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions