| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
kernel typing.
|
|
|
|
|
|
|
|
Upper layers are still not able to handle mutual records though.
|
|
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
|
This is a first step towards the acceptance of mutual record types in the
kernel.
|
|
|
|
|
|
|
|
|
|
|
|
It was used in some examples, but never fully documented
|
|
|
|
- we always rename
- we compile {clear}/view to /view{clear}
|
|
|
|
|
|
|
|
|
|
|
|
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
|
|
|
|
understands.
|
|
|
|
forward-line.
|
|
|
|
|
|
|
|
|
|
|
|
directory
|
|
|
|
When initilazing the load path, coqtop adds implicit bindings for stdlib
and for the current directory (-R stdlib Coq -R . ""). In case of
a clash, the binding of the current directory had priority, which makes
it impossible to edit stdlib files (when they Require files from the
same directory) using PG, or from CoqIDE when launched from the directory
containing the file.
Example to reproduce the problem:
```
cd plugins/omega
coqide Omega.v
```
some of the Requires will fail.
|
|
|
|
|
|
|
|
induction schemes
|
|
|
|
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear
who wrote it and why it was introduced in the first place.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
example PR.
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
