aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInModule.v
diff options
context:
space:
mode:
authorHugo Herbelin2015-06-23 19:24:22 +0200
committerMatthieu Sozeau2016-06-02 14:07:32 +0200
commitf086aed126f63d2db76be876d387beb8915d381a (patch)
tree3ba161b2de8664e2bdea15094a36035496eaed67 /test-suite/output/ErrorInModule.v
parent4a1ed5becf04dfa6dde6d7464d913c6f1f6340ff (diff)
Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions