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...
Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4950 From: @JasonGross Reported version: 8.6 CC: @herbelin, @ppedrot Blocker for: [BZ#5056](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%235056%22)
When stopped in the debugger, display goals in the same format used when CoqIDE is not in the debugger. Redisplay goals in the debugger when the user changes display options...
The changelog constains "DOC TODO" a few times. Check if it is really the case that the documentation is missing.
We should add https://github.com/liyishuai/coq-http to the CI. As recommended here: https://github.com/coq/coq/pull/15333#discussion_r884178848. Although I am not sure we would be able to catch the issue with extraction on an older version...
Packages loaded from the `user-contrib` directory and from `COQPATH` are loaded with `-Q` even if `_CoqProject` specifies `-R`. If the user has `-R` in their _CoqProject file, some `Require` commands...
#### Version Coq 8.7.1 #### Operating system macOS 10.12.6 Sierra #### Description of the problem The hint engine treats the following two hints differently, namely with `Hint Resolve` the engine...
#### Description of the problem `repalce` fails to progress because such a replacement will break typechecking. ```coq Axiom x : nat. Axiom y : nat. Definition z := x. Goal...
Closes #15936 - [x] Added **changelog**. - [x] Added / updated **documentation**. - [ ] Opened **overlay** pull requests (hopefully none necessary).
@Alizter your lengthy comments [here](https://github.com/coq/coq/pull/15888#discussion_r896666832) were a bit overwhelming. My question was: > What is your command line to `make` for the coq_makefile-generated makefile? But I think my real question...
Don't know if it is related, but recently, I started to need to pass an explicit `-coqlib` to `coqtop` in `coqdev-ocamldebug` for emacs (otherwise I get the "cannot guess ..."...