aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInModule.v
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-12 22:37:33 +0100
committerEmilio Jesus Gallego Arias2019-02-23 16:53:53 +0100
commitd31056ec924ef6e09b28bc3822b427b67a8a300b (patch)
treed720333732d9be1a03f74cc079e0a1903d31e023 /test-suite/output/ErrorInModule.v
parentc37e90b67c74b32837409a9a424757246067ef1b (diff)
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions