diff options
| author | Arnaud Spiwack | 2014-11-27 17:10:46 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-28 19:21:24 +0100 |
| commit | ea0444233d08b624c2e9caaee74ea8f3b6625710 (patch) | |
| tree | 3335f671d8e2cfdc070d510eca730aedb576f1cd /dev | |
| parent | 34815f0c8fae4c87798b18f7343c1f1afc3056eb (diff) | |
Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.
When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.
Fixes test-suite/success/apply.v
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions