aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-07 14:14:04 +0100
committerGaëtan Gilbert2019-02-12 17:16:39 +0100
commit68f3d842f6a9652cadf0698f54117fdc24172ac7 (patch)
tree9058830691275650cf58f461a34749afc8a018ee /dev/include
parenta9fbbfc53a7d7dcd5245960a0e3a2d2d7b6b8695 (diff)
Fix failing coqtops in tactics.rst
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions