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...
We can use `rewrite lem by tac` to rewrite with lemma `lem` and resolve side conditions by tactic `tac`. But I cannot find its counterpart in `rewrite_strat`, e.g. `rewrite_strat bottomup...
> While we're talking about this, I think the way we handle the VM in the checker is completely nonsensical. Basically we trust whatever code found in the vo, which...
### Description of the problem [This concerns pretty-printing in Coqdoc.](https://coq.inria.fr/doc/master/refman/using/tools/coqdoc.html?highlight=coqdoc#pretty-printing) The printing directive must appear at the top of the file before other comments, or it does not work correctly....
### Is your feature request related to a problem? Currently, Coq extraction does not support functions with nontrivial sort polymorphism (instantiations using `Prop` or `SProp`), as can be seen in...
### Description of the problem In Coq 8.20 and later, functions that (somewhere) use SSReflect's `have` tactic opaquely (the standard use which means using `ssr_have_upoly`) cannot be extracted, and fail...
**Kind:** cleanup, fix This PR does the following: - it fixes #5698 (simpl unfolding a primitive projection even if told not to unfold it) - it parametrizes the code of...
See https://github.com/ocaml/opam/issues/3435 for more details about this 6 year old bug.
This PR ensures that `simpl never` strongly forbids the reduction of terms in position of argument of `match`, `fix` or a projection for `simpl`, as e.g. in: ```coq Record T...