diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-06-04 15:47:28 -0700 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-07-01 15:42:25 -0700 |
| commit | 313e6bed17b400d638401a5c6e5d442eadb73d3a (patch) | |
| tree | 494b64ac86538e07216c5da59315168688935c6f /plugins/extraction/ExtrOcamlIntConv.v | |
| parent | 033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff) | |
Implement uniform parameters in ComInductive
Don't allow notations attached to uniform inductives
Diffstat (limited to 'plugins/extraction/ExtrOcamlIntConv.v')
0 files changed, 0 insertions, 0 deletions