diff options
| author | Matthieu Sozeau | 2016-10-29 19:07:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-03 16:26:40 +0100 |
| commit | f6916774eea2ecc1262377cb14c2d494a0486358 (patch) | |
| tree | fde2d5865f5d5e1201de86692135d785b086a55b /tactics/class_tactics.mli | |
| parent | d51c384e52003668bd97ca44da77a14c91e5cb14 (diff) | |
Do not shelve non-class subgoals but fail, it should
be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
Diffstat (limited to 'tactics/class_tactics.mli')
0 files changed, 0 insertions, 0 deletions