diff options
| author | Hugo Herbelin | 2014-12-04 11:38:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-04 16:19:17 +0100 |
| commit | e11854569b855ae4d675e560d807ec14b8b607bf (patch) | |
| tree | b5ffa735f1c5f5ef5317fe3f70c645ab3c2c8894 /dev/include | |
| parent | 964024bf87a87b0e87d8891b3090083ea49b1d03 (diff) | |
Trying a new policy for when to automatically print goals (granting
the non-verbose mode which I guess one wants to obey whatever
interface is used, and restoring a policy ok for coqtop - maybe would
need a change if obeying the local verbose flag is not ok for PG or
Jedit).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions