aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorVincent Laporte2018-10-09 11:30:54 +0000
committerVincent Laporte2018-10-09 11:30:54 +0000
commit1577a12cab63cdccf5b37253072192ecec5a752c (patch)
treed76e8a7b3388ed3314154d651ef3980fd4a30a6e /plugins/syntax
parent3537f1c43098e35636d3982466172ab66720b035 (diff)
[coqchk] Fix checking of records in module signatures
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions