diff options
author | 2015-12-21 11:37:06 +0100 | |
---|---|---|
committer | 2015-12-22 16:25:20 +0100 | |
commit | e1ac3467db26f9bcc09f12989eeb8379c4fc5817 (patch) | |
tree | e9c46f9944c414cda11513188903839131b9c582 /tactics | |
parent | b88929d9d8de179a7e356cf9cbe2afef76f905a3 (diff) |
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions