| Age | Commit message (Collapse) | Author |
|---|
|
coretactics.ml4.
|
|
replay nodes]
|
|
|
|
|
|
size.
|
|
|
|
|
|
supported scenarios.
|
|
Example not yet fixed by this patch:
```
Definition u : Type.
Definition m : Type.
exact nat.
Defined.
exact bool.
Defined.
```
|
|
|
|
|
|
Noticed by Sigurd Schneider.
|
|
|
|
|
|
|
|
|
|
|
|
`Drop` is implemented using exceptions-as-control flow, so the
toplevel state gets corrupted as `do_vernac` will never return when
`Drop` occurs in the input.
The right fix would be to remove `Drop` from the vernacular and make
it a toplevel-only command, but meanwhile we can just patch the state
in the exception handler.
We also need to keep the global state in `Coqloop` as the main
`coqtop` entry point won't be called by `go ()`.
Fixes #6872.
|
|
We test the 3 possible scenarios. A more complete test would also
involved fake_ide.
c.f. #6793
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Ring_theory.v)
|
|
|
|
|
|
infinite eta-expansion)
|
|
get_lexer_state.
|
|
by Travis.
|
|
|
|
|
|
|
|
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
|
|
|
|
|
|
|
|
This completes the work of
b60906cc3ee3f994babf9cceff2971bd03485f2f
|
|
As per https://github.com/coq/coq/pull/6756/files#r168028764
|
|
|
|
|
|
|
|
|
|
|
|
|
|
serialization.
|
