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 is a work in progress; is someone from @coq/ltac2-maintainers willing to help me complete the OCaml side of this? - [ ] Added / updated **test-suite**. (is this needed?)...
#### Description of the problem I'd like some help figuring out what's going on here. Roughly the thing going on is that I'm creating something roughly analogous to `@id _...
According to suggestion in issue #16479 the following lemmata have been added: * in coq/theories/Logic/FinFun.v: + Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A. + Lemma Finite_dec {A:Type}:...
We remove the "library location" information bit as it is only used for printing and introduces a dependency on `Library` which is unnecessary, as in my opinion we'd like loadpath...
The `Arguments` command only supported at most one scope for each argument. This PR enables multiple scopes. This would be useful for instance in MathComp where we'd like to bind...
We add an `Extraction Output Directory` option that defaults to the current directory for extraction. This is meant to address: - https://github.com/coq/coq/issues/9148 We "kind of" have a command line option...
If I only have `coq-core` installed, given `MyCoqFile.v` ``` Declare ML Module "ltac_plugin". ``` Running ``` coqc -noinit MyCoqFile.v ``` errors out with ``` cannot guess a path for Coq...
This might be the same issue as https://github.com/coq/coq/issues/10941 and those linked there, and/or those with label "wellknown: ltac variable bypasses typechecking", but I couldn't find any existing report with an...
It was basically a noop since the move to dune.
This way we can import them separately from the boolean operators. We name it `BoolNotations` after `Coq.Lists.List.ListNotations`. - [ ] Added / updated **test-suite**. (nothing to do?) - [x] Added...