coq
coq copied to clipboard
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
I've been observing huge parsing slowdowns in interactive use for a while, and I finally found out that these are due to physical equality in `share_tails` missing a lot of...
This is needed to implement caching of parsing. Tested. - `Parsable.loc`: determine current position - `Parsable.consume`: advance the stream on a cache hit.
In the messages panel, the warning appears twice. The server is sending the message twice (I checked). This may be a small inconvenience for users, but would be nice to...
This is based on the discussion here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/reduction.20in.20the.20kernel It should be completely backwards compatible. I would like to get a benchmark run to determine if there is any impact. The...
#### Description of the problem In Coq 8.11.1, a 'replace' command causes the Qed to blow up (I killed it after 1 hour), but without the 'replace', the Qed takes...
Fix #16410 (there may still be some that don't get caught)
#### Description of the problem The coqtop REPL has no documentation on how to exit it. It turns out you can exit the REPL with `Quit.` and `Ctrl-d` but it...
#### Description of the problem Here's the example program: ```coq From Ltac2 Require Import Ltac2. Ltac2 Eval () 1. ``` Here's the error message: ``` File "./test4.v", line 2, characters...
I guess gcc updated and now I get this: ~~~ gcc kernel/byterun/coq_interp.o coq_interp.c: In function ‘coq_interprete’: coq_interp.c:301:20: warning: storing the address of local variable ‘coq_lbl_ACC0’ in ‘coq_instr_base’ [-Wdangling-pointer=] 301 |...