| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
rules
|
|
|
|
|
|
|
|
|
|
dev/doc/changes.
|
|
|
|
|
|
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
|
|
This finally closes #5994.
|
|
After `Drop`, `Coqtop.drop_last_doc` will contain the current document
used by `Coqloop`. This is useful for people wanting to restart Coq
after a `Drop`.
|
|
|
|
|
|
|
|
|
|
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
|
|
|
|
|
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
We use git check-attr to look at the same files as git diff --check.
|
|
|
|
|
|
|
|
|
|
This follows the merge of AbsInt/CompCert#191.
|
|
just Iris
|
|
|
|
|
|
|
|
|
|
|
|
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
See also GeoCoq/GeoCoq#7.
|
|
|
|
|
|
|
|
|
|
|
