diff options
| author | Matthieu Sozeau | 2016-11-15 13:53:57 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-15 14:54:05 +0100 |
| commit | 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 (patch) | |
| tree | ade3adfabf9e288a164769e0457fda6e49ac1b24 /dev/base_include | |
| parent | dfefd12ee432e5b0d145934e74bb939ddecfa522 (diff) | |
Revert part of a477dc, disallow_shelved
In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.
Fix test-suite now that shelved goals are allowed
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions