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 commit adds the ~2000 non-spacing marks into the IdentPart category. This includes all the combining marks, and thus fixes #19512. This also means that characters in the range 1DC0-1DFF...
### Description of the problem Coq accepts Unicode characters with embedded diacritics as identifier characters. Coq also accepts characters from the Combining Diacritical Marks Supplement block (0x1DC0 roughly through 0x1DFF)...
### Description of the problem The magic function below should be extracted as "let rec magic x = magic x". Instead it is extracted as "let rec magic = magic"...
### Description of the problem When defining mutual fixpoints at toplevel, the first fixpoint can be extracted but trying to extract the second one triggers an anomaly. Error: Anomaly "reference...
Hint Resolve registers the same hint for a definitional class multiple times at different patterns
### Description of the problem `Hint Resolve` is a little overeager and finds multiple possible patterns for hints whose type ends in definitional classes. `Existing Instance` does not have this...
This file uses a lot shadowing, which makes it hard to understand. Suffix top-level functions that return `_ Ftactic.t` with "_ftactic" instead of using shadowing (this way the external interface...
For example: ``` Hint Extern 1 => split : plus. Goal 1=1 /\ 1=1 /\ 1=1 /\ 1=1. info_auto 10 with nocore plus. (* info auto: *) split. split. split....
With #19092 and #19322, we can now see `Derive` statements as non-recursive telescopic blocks of theorems and take the standard now-unified route in use for `Definition` and `Theorem`. As a...
### Description of the problem https://github.com/coq/coq/pull/19049 introduced new warnings. These warnings should be disabled for "printing only" notations since parsing is irrelevant there. This issue shows up with the proofmode...
### Description of the problem I am getting a warning about incompatible notation, but it is not clear to me why the notation should be incompatible, and the notation has...
