| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
|
|
|
|
|
|
|
|
|
|
|
|
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}
|
|
|
|
|
|
|
|
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
|
|
|
|
|
|
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
|
|
|
|
understands.
|
|
|
|
forward-line.
|
|
|
|
|
|
|
|
|
|
|
|
directory
|
|
|
|
I think the bug was introduces when apply_type was made safe.
In the test joint to #7255 rewrite (setoid case) generates an
ill-typed goal and apply_type raises a Pretype_error.
It is unclear to me why the tactic monad does not turn the
pretype_error into a UserError
|
|
|
|
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.
|
