| Age | Commit message (Collapse) | Author |
|---|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
|
|
|
|
|
|
|
|
The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).
We also add a `-bytecode-compiler` flag.
Fixes #4607
|
|
|
|
|
|
|
|
|
|
Made possible by the previous commit passing ~evars to
check_hyps_inclusion.
|
|
|
|
|
|
We know that the two are living in a common type, so that it is useless
to perform the comparison check. Note that we only use this fast-path when
the branches are only made of lambda-abstractions, but this covers
all actual cases.
|
|
They are only used once, thus it is completely useless to reallocate arrays
that are going to be destructed immediately.
|
|
No reason to split the code, this function is only used once.
|
|
|
|
entries
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I looked for this information and forgot about it a couple times so
let's put it in writing.
|
|
|
|
|
|
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
|
|
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
Also updated the comments.
|
|
|
|
Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
|
|
This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.
|
|
This file is already mostly in the required style so I wanted to see
what it looks like.
For a couple matches I locally disabled the warning as it was too
annoying otherwise (`when` clauses are especially annoying).
There are a couple places where I think it clearly looks better (eg
assoc_defined at the beginning of the file) but overall I'm not all
that convinced.
What do other people think?
|
|
It's basically an occur check so it makes sense to put it in vars
|
|
Such a basic function can live in Univ rather than the higher level UnivGen.
|
|
|
|
|
|
|
|
mind_of_delta_kn + functional version of is_polymorphic
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
This is to move a standard combinator to the place it belongs to. An
alternative could have been to put it in termops.ml, but termops.ml is
now about econstr, so, even if it makes the kernel "bigger", constr.ml
seems to be the best place for this combinator. After all, this
combinator is canonical.
|
|
|
|
|
|
We take advantage of the separation of implementation from CBV to remove
constant code.
|
|
|
|
We favour unfolding of variables over constants because it is more frequent
for the former to depend on the latter. This has huge consequences on a few
extremely slow lines in mathcomp, up to dividing by 3 single-line invocations
that were taking about 30s on my laptop before the patch.
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
Just like in the Sixth Sense, it turns out it was dead code all along.
|
