aboutsummaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-31 18:15:09 +0200
committerPierre-Marie Pédrot2017-08-31 18:15:09 +0200
commit40edf6a111ae2b9f0a230c2617b3e86e8fbfa6dd (patch)
tree6d81bde058ad791078e77c1e5a00226c2d847b4b /tests
parent84047666ce13f1eec440d38d9784ae125612507c (diff)
Fix coq/ltac2#3: Constructor expects n arguments should name which constructor it is.
Diffstat (limited to 'tests')
0 files changed, 0 insertions, 0 deletions