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...
Fixes / closes #18572 - [x] Added / updated **test-suite**. - [x] Added **changelog**.
This makes it possible to capture the location of notation arguments. Typically `apply` wants the location of the constr argument so that it can report type mismatches at that location....
#### Description of the problem I'm writing an EDSL in Coq. Users write untyped programs, which are then typechecked. At the moment, when a program contains a type error, I...
This was left as future work in https://github.com/coq/coq/pull/14037 due to increased power of zify breaking a few CI developments; I have now managed to get everything that builds with my...
This is to test whether the new semantics might make more sense in practice. If so, it could be an answer to the current time explosion in [#18617](https://github.com/coq/coq/pull/18617#issuecomment-1970826947). Note: a...
The PR adds the following: - if `x` is a projection, `About x` indicates it - if `x` is a projection, `Print x` prints the whole record to which this...
I just coached a new Coq user to work around this incompleteness; it didn't leave a good impression. - [ ] Added **changelog**. - [ ] Opened **overlay** pull requests...
Whether `hnf` should grant `simpl never` is unclear. In practice: - it follows what `simpl` does on named fixpoints and named cofixpoints as well as on terms hiding a projection...
Eventually we want to get rid of all delayed_of_tactic uses but let's take it one step at a time. This should not be particularly impactful as we need to eg...
Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4261 From: @ppedrot Reported version: 8.5 CC: @silene
