| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
subtyping.
|
|
|
|
Not sure it could have led to a soundness bug, but this is definitely
serious enough to deserve a backport. Also made the code robust by
listing all the constructors.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
When inferring [u <= v+k] I replaced the exception and instead add
[u <= v]. This is trivially sound and it doesn't seem possible to have
the one without the other (except specially for [Set <= v+k] which was
already handled).
I don't know an example where this used to fail and now succeeds (the
point was to remove an anomaly, but the example
~~~
Module Type SG. Definition DG := Type. End SG.
Module MG : SG. Definition DG := Type : Type. Fail End MG.
~~~
now fails with universe inconsistency.
Fix #7695 (soundness bug!).
|
|
Not sure if worth using in other places.
|
|
|
|
It was used in some examples, but never fully documented
|
|
|
|
- we always rename
- we compile {clear}/view to /view{clear}
|
|
|
|
|
|
|
|
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
|
|
|
|
|
|
INSTALL.doc.
|
|
Relative links. Cf. #7800.
|
|
[ci skip]
|
|
- Fix the Markdown.
- Add link to latest build of the refman for the master branch.
- Clarify what are the dependencies of the HTML doc.
[ci skip]
|
|
This will avoid in particular this ambiguous file extension.
[ci skip]
|
|
|
|
|
|
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
|
|
|
|
understands.
|
|
|
|
|
|
forward-line.
|
|
|
|
|
