aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorQuentin Carbonneaux2020-05-07 10:43:14 +0200
committerQuentin Carbonneaux2020-05-07 10:43:14 +0200
commitbec12fd4c5126987229716d6ca1fb73be458e903 (patch)
tree07bcd8031c9220f9b54c17a2b36f8746511014ca /dev
parent8c2bd9df97972d47554a87c36f5397b514d30cde (diff)
Drop some the coqtop output, rephrase a bit
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions