diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 23:26:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 18:14:54 +0100 |
| commit | f5abd069a86b85829ab49141d27ef7633f4b84a1 (patch) | |
| tree | f8855946b56d03188a6415e81cbf94cdde2ae0b2 /printing | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
[toplevel] [vernac] Remove Load hack and check supported scenarios.
Parsing in `VernacLoad` was broken for a while, but the situation has
improved by miscellaneous refactoring.
However, we still cannot support `Load` properly when proofs are
crossing file boundaries. So in this patch we do two things:
- We check for supported scenarios [no proofs open at `Load` entry/exit]
- Remove the hack in `toplevel` so the behavior of `Load` is
consistent between `coqide`/`coqc`.
We close #5053 as its main bug was fixed by the main toplevel
refactoring and the remaining cases are documented now.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions