aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-19 14:33:19 +0100
committerGaëtan Gilbert2020-04-13 15:18:18 +0200
commitbbcf08fe1c0ab7e2cf21711f56230aaae93a1bdb (patch)
tree4f1cb9c7878df65842f013d25951fd7fddc41ddd /checker
parent0beca74bc90cef03d779a8e4f8668335c9c37716 (diff)
Add specific test for "useless" syndef
This happens in practice with the list syndef in List.v
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions