aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorHugo Herbelin2015-02-08 10:20:39 +0100
committerHugo Herbelin2015-02-10 21:56:06 +0100
commitf804e681f1550e1c20b8ce5b83bc66c876fb3c99 (patch)
treed112771be4296cd091b3e2128e8603487bac2420 /dev/include
parent02d2cdf61f6c6a37a1bda25d738a0d189a4021a6 (diff)
Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coqtop mode.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions