aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-07 11:45:10 +0100
committerGaëtan Gilbert2019-02-12 14:39:49 +0100
commitf78d36363698f653ff8ff16389c58633579493eb (patch)
treeccb405e08c030473867c6085a459d3d9ab9e7b0b /dev/include
parent146a9d73bd5ceff18e08d36d942dca874f388d5c (diff)
Fix failing coqtops in extended-pattern-matching.rst
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions