aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
diff options
context:
space:
mode:
authorJasper Hugunin2018-06-04 15:47:28 -0700
committerJasper Hugunin2018-07-01 15:42:25 -0700
commit313e6bed17b400d638401a5c6e5d442eadb73d3a (patch)
tree494b64ac86538e07216c5da59315168688935c6f /dev/tools
parent033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff)
Implement uniform parameters in ComInductive
Don't allow notations attached to uniform inductives
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions