| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
tactics is broken
|
|
|
|
|
|
broken
|
|
|
|
This has been in OCaml since 4.04.
|
|
module
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
|
|
|
|
For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.
I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
|
|
|
|
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
|
|
|
|
Now that the checker is using the regular kernel files it can also use
the normal printers.
|
|
|
|
|
|
|
|
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing
changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
|
|
|
|
for pretyping"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is the first release that contains the type-safe grammar API.
|
|
This reverts commit 8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a.
Fix #7936
# Conflicts:
# proofs/clenvtac.ml
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section of CHANGES.md.
|
