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...
A short PR preventing a `List.last` anomaly regression in the current situation: ```coq Fixpoint f : nat. ``` - [x] Added / updated **test-suite**.
The PR simplifies `Theorem with` and makes it more flexible: - We accept, if coinductive, that the conclusions have the same or different coinductive types in any order. - When...
The `using` clause was stored either in the `Proof.t` (for definitions generating proofs) or in the `CInfo.t` (for definitions with immediate proof, one for each component if a co/fixpoint). The...
The PR fixes ```coq Fixpoint f (n:nat) : nat where "- n" := (f n). ``` which was failing with `f` not found beforehand. - [x] Added / updated **test-suite**.
Who has experience with `rapply`? Shouldn't it be at some time the default `apply` (or, at least, unifall would lead to identify apply and rapply, right?)? There is an alternative...
DO NOTE MERGE: Waiting to be rebased on Coq/Coq#19144 once/if it is merged. Removing "Include Type" which was deprecated since 8.3. "Include" now supports "Include type
This allows writing a tactical that catches (non-monadic) system exceptions during the execution of a tactic. As a proof of concept, we introduce the Ltac tactical `catch_stack_overflow`. I think that...
Tentative fix for #18332. If the patch is accepted I will add a test in the bench too.
`find -exec grep` is very slow compared to `grep -l` which does the same thing.
#### Description of the problem ```coq Require Import ZArith Lia. Local Open Scope Z_scope. Goal forall (a b c : Z) (n : c = 0 -> False) (q q0...
