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...
This prevents loading in memory potentially useless data, especially the so-called "structured values" which are (potentially big) blobs. As per the bench, the size of vo files is basically unchanged.
During a very bizarre proof script, when Coq is running as `coqidetop`, a `Subgoals` request (with `fg = false`, `bg = shelved = given_up = true`) hits a Not_found. The...
Fixes https://github.com/coq/coq/issues/17463 (but for `fail`, only supports plain string messages, but no printf-style messages, because that seems not possible in a reasonable way) - [X] Added / updated **test-suite**. -...
Fixes / closes #17583. We are a bit less eager to define every terminal of a `Tactic Notation` as a keyword, following what we already did for `Notation`. We make...
This is a by-product of #17392, going in the direction of improving the API of `cUnix.ml`, to be discussed with @ejgallego. At the current time: - it fixes a bug...
This is an experimental PR going in the direction of manipulating only folded primitive projections. Both fMATCH/fCOFIX and fPROJ are required to reduce the projection of a record value and...
This also exposes the `Tac2core.get_map` function, without which it is not possible to add new `set/map` functions from a plugin. - [x] Added / updated **test-suite**. - [x] Added **changelog**.
Here is a bunch of small improvements to menu items and accelerators. - Add “Open” to the toolbar - Add “Fully check” to the Navigation menu - Avoid overlapping accelerators...
Morally we consider them part of the body univs. This makes it so we don't need to disregard keep_body_ucst_separate when there are side effects. Fix #18636 (alternative to #18640, but...