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...
Preliminary PR to #19290 Includes the less controversial half of the above, to split reviewing work
Overlays: - https://github.com/impermeable/coq-waterproof/pull/140
Add documentation for tactic `ensatz` introduced by [PR](https://github.com/rocq-prover/stdlib/pull/160) - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new / changed **user messages**....
### Description of the problem [Passing version from 3 weeks ago](https://github.com/mit-plv/fiat-crypto/actions/runs/14977402102/job/42078833780) (de8e6e97603ac2853a88438192821491a8b3163e): [ExtractionHaskell-source-master-de8e6e97603ac2853a88438192821491a8b3163e-passing.zip](https://github.com/user-attachments/files/20596554/ExtractionHaskell-source-master-de8e6e97603ac2853a88438192821491a8b3163e-passing.zip) [Failing version](https://github.com/mit-plv/fiat-crypto/actions/runs/15369438942/job/43248316649) (8c1f088465175e27a87dd6dd38c063cdc53a1a8c): [ExtractionHaskell-source-master-8c1f088465175e27a87dd6dd38c063cdc53a1a8c-failing.zip](https://github.com/user-attachments/files/20596555/ExtractionHaskell-source-master-8c1f088465175e27a87dd6dd38c063cdc53a1a8c-failing.zip) GHC version: The Glorious Glasgow Haskell Compilation System, version 9.12.2 Error: ``` command...
I went through https://rocq-prover.org/doc/master/refman/coq-tacindex.html in order (skipping SSR tactics), adding the easy ones and adding a TODO comment for the rest. (currently stopped after "d" tactics)
Fixes / closes #20044 - [x] Added / updated **test-suite**. - [x] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new / changed **user...
Fixes / closes #18259 #20155 - [X] Added / updated **test-suite**. - [x] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Opened **overlay** pull requests.
~~~coq (* -*- coq-prog-args: ("-allow-sprop"); -*- *) Axiom T : SProp. Axiom a b : T. Goal forall P, P a -> P b. intros P v. vm_compute. (* inserts...
### Description of the problem Seems like this warning was not intended for this example and should not appear. The example should be changed to eliminate it. See https://rocq-prover.org/doc/master/refman/addendum/rewrite-rules.html#higher-order-pattern-holes ...
Fixes / closes #???? - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new /...
