diff options
| author | Cyprien Mangin | 2018-01-19 11:12:06 +0100 |
|---|---|---|
| committer | Cyprien Mangin | 2018-01-22 11:09:12 +0100 |
| commit | a6a1cf208ddc89b06b67f13f4291dc944534684a (patch) | |
| tree | 9575cd4cce9a2f2f970a5298e5c3ac3cfc8bb788 /kernel/nativelambda.ml | |
| parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) | |
Fix #6591: anomaly when using selectors outside of a proof.
When asking for a hint about bullets, we check
that there is an ongoing proof.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions