| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
| |
| |
| |
| |
| |
| | |
Part of this code has been introduced very recently in 7c62654 in spite of
the existence of a proper API. This means that this should be better
documented.
|
| | |
|
| | |
|
| |
| |
| |
| | |
The concrete syntax is still restricted to identifiers.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|/
|
|
| |
Elaborate a [atts] record out of a list of flags.
|
|\ |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
|\ \
| | |
| | |
| | | |
points of Camlp5
|
| | | |
|
| | |
| | |
| | |
| | | |
Don't allow notations attached to uniform inductives
|
| |/
|/|
| |
| |
| |
| |
| | |
Fixes: #7915.
Due to a change in the original misctypes removal PR, the deprecation
notice went out of sync.
|
|\ \
| | |
| | |
| | | |
format).
|
|\ \ \
| | | |
| | | |
| | | | |
break hint).
|
| | | | |
|
| | | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
| |/ |
|
|\ \
| | |
| | |
| | | |
constr in Constr
|
| |/
|/| |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| | |
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
constants
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
obligations.
|
| |_|/ /
|/| | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
subtyping.
|
|\ \ \ \ \ |
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | | |
Highly spaghetti code, hopefully works.
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | | |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| |_|/
|/| |
| | |
| | |
| | |
| | | |
The universe context was dropped even though it isn't added to the
global universes yet. Keep it so that it is properly defined with
the constant the expanded obligation appears in.
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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!).
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
induction schemes
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|\ \ \
| | | |
| | | |
| | | | |
of submodules.
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Currently, if one of the inductives is non recursive, it defaults to a
case analysis schems taking fewer predicates and methods just for that
inductive. This irregularity prevents doing a combined scheme afterwards
to gather all eliminators into one, as combined scheme expects all the
eliminators to have the same predicates and methods. I have a use case
in building function graphs in Equations where some of the inductives
might not be recursive but I expect many other use cases could exist.
|
| | |
| | |
| | |
| | | |
To be removed in 8.10.
|
| | |
| | |
| | |
| | | |
We move the last 3 types to more adequate places.
|