| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| |/
|
|
| |
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"
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Primitive projections were not correctly unfolded, leading to failure of
conversion checks in some cases. The kernel was strangely not affected by
this bug, and it was probably a remnant of some vestigial code.
|
| | |
|
| |
|
|
|
| |
We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
|
| | |
|
| |
|
|
|
|
| |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
| |
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
This was redundant with ZcaseT, the only difference lying in the use or not
of fclosures for substerms. This code was removed from the kernel in commit
f2f805ed, we finish the work in the checker now.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Before this patch, passing a mere identifier (without dots) to the checker
would make it consider it as implicitly referring to a relative name. For
instance, if passed "foo", it would have looked for "Bar.foo.vo" and
"Qux.foo.vo" if those files were in the loadpath.
This was quite ad-hoc. We remove this "feature" and require the user to
always give either a filename or a fully qualified logical name.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
It is not doing the same thing as coqtop, and the corresponding coqtop
semantics is irrelevant in the checker as the latter does not rely on ML
code.
|
| | |/
|/|
| |
| |
| |
| | |
It has exactly the same effect as -R, because there is no such thing as
implicit relativization for object files in coqchk, contrarily to what
Require does in coqtop.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Instead of relying on the OCaml demarshaller, which is not resilient against
ill-formed data, we reuse the safe demarshaller from votour. This ensures that
garbage files do not trigger memory violations.
|
| |/
|
|
|
| |
This allows to work around the size limitation of vanilla OCaml arrays on
32-bit platforms, which is rather easy to hit.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| | |
| |
| |
| |
| | |
Making it bigger is kind of useless, takes time and clutters the output for
no real advantage.
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| | |
This will allow to merge back `Names` with `API.Names`
|
| |/
|
|
|
| |
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
|
Maxime Dénès
Matthieu Sozeau
Emilio Jesus Gallego Arias
mrmr1993
Théo Zimmermann
Jim Fehrle
Pierre-Marie Pédrot
Gaëtan Gilbert
Ralf Jung