aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/pre-commit
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-07-12 18:05:46 +0200
committerPierre-Marie Pédrot2018-10-02 09:27:47 +0200
commit278f64296af13865ed50c966f1a4c1ab4357423e (patch)
tree47fdae130f40342f8f9439cddc3aac46b1c0c528 /dev/tools/pre-commit
parent67e894bc9e25e68bb89c93c930d3c9eac3f8a16d (diff)
Port g_derive to coqpp.
Unluckily this is the only file that contains a VERNAC EXTEND and no ARGUMENT EXTEND, which are not handled yet.
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions