| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\
| |
| |
| | |
subtyping.
|
| | |
| |
| |
| |
| | |
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!).
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| | |
This eliminates 3 uses of Obj from TCB.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| | |
| |
| |
| |
| |
| | |
This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
|
| |/
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| |
|
|
|
|
|
|
|
|
| |
Unluckily, this is completely wrong as we trust the inlined term to be
well-typed in some unavailable environment. To start with, the checker
should not even rely on substitutions as it does not trust functors,
but it does anyways. I have thus commented this code as a useful backdoor
for when Coq is used to implement the next blockchain Ponzi scheme.
We really need to sort this out though.
|
| |\
| |
| |
| | |
coinductive types.
|
| | |
| |
| |
| |
| | |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| |\ \
| | |
| | |
| | | |
global env
|
| |\ \ \
| | | |
| | | |
| | | | |
in CArray
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
instances
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.
|
| | |_|/
|/| | |
|
| | |/ |
|
| |/ |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
| |
Makes printing rules more explicit and should close #6799.
|
| | |
|
| |\ |
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
constraints.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
camlp4
|
| | | | | |
| | | | |
| | | | |
| | | | | |
longer use camlp4.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| | | |/ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| |/
|
|
|
|
|
|
|
|
| |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
| |
|
|
| |
This just shares the unfold_projection between Closure and Reduction.
|
| | |
|
| |
|
|
| |
Fixes #5747: "make validate" fails with "bad recursive trees"
|
| | |
|
| | |
|
Gaëtan Gilbert
Matthieu Sozeau
Pierre-Marie Pédrot
whitequark
Hugo Herbelin
Emilio Jesus Gallego Arias
Maxime Dénès
Matthieu Sozeau
mrmr1993
Théo Zimmermann
Jim Fehrle