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...
#### Description of the problem In particular it's not clear what the difference is between `let x := f () in Control.refine (fun () => x)` and `Control.refine f`. (And...
@ejgallego Have a look at this dummy PR: https://github.com/coq/coq/pull/16491 For some reason, tarballing the _build dir seems to be triggering a rebuild but only for our coq rules. To be...
We remove from the API stuff that is exported but clearly internal details, and enforce a few invariants by typing.
Remaining users: - `par:` - Program (in `obligation_terminator`) - ssr (a lot)
Update syntax and descriptions in the tactics chapter.
This is a followup on the discussion I started here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Discharging.20proof.20states Summary: Since 8.16, the function `Cooking.expmod_constr` has disappeared due to https://github.com/coq/coq/pull/14727, which breaks my plugin. So I'd like to...
After `[foo] : simpl`, `foo` is no longer marked as shelved. `Unshelve` won't make it visible. This doesn't happen with `[foo] : idtac` or `[foo] : auto`. ```coq Goal forall...
**Kind:** tentative enhancement of unification + fix We check typability of the resulting first-order unification problem before trying first-order heuristics. We use retyping which should be rather quick. Maybe the...
Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#5341 From: @tchajed Reported version: trunk CC: @tchajed
