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...
Those who want the old behaviour can use Control.refine with a manual thunk. Close #18522
Close #18637 To be decided: - should we warn for variable names starting with `_`? (current code does) - should we split the warning like ocaml does (unused `let x...
Fix #18697 We could fix filter_or to avoid breaking physical equality instead but assuming the bench does't complain I think using semantic equality is nicer.
- there is an implicit `once` - windows has timeout since 81c8acb84510de54424330ee83e4852e7610e27b AFAICT
**Kind:** cleanup This PR is a step towards merging the different paths for `Context` and `Variables` (and their variants). It includes - relying on a generic `interp_named_context_evars` to interpret contexts...
This PR clarifies some differences between `cbn` and `simpl`, especially with respect to how `simpl never` is taken into account. See discussion at #18581 for the non-impact of `simpl never`...
The overlay infrastructure now supports declaring that the root directory of some builds is a subfolder of a given repository. This allows overlay-writers to override the repository and branch (and...
In case there is a wish to eventually remove `Cd` (which does not make sense is a relocatable document). Closes #16119. Depends on #17392 and #16126 (merged). - [ ]...
Demo here: https://github.com/Zimmi48/coq/issues/new/choose (feel free to go all the way and create new issues to see how it goes) I'm opening this PR to get feedback: - What do you...
~Requires https://github.com/coq/coq/pull/18349 (merged)~ Following a few discussions on Zulip, it seems nice to warn new users about the fact that this part of the standard library is no longer state...
