| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
It is not clear that this is really needed, but in case it happens,
one will at least have a partial result available rather than an
unexploitable global failure of the parser.
|
| | |
| |
| |
| |
| |
| |
| | |
Indeed, the debugger debugs coqtop but it is itself just an ocaml
runtime extended with the coq printers. It does not know the
environment, so, looking in the Global.env() for the printers can only
fail.
|
| |/
|
|
| |
This is a first step towards some of the solutions proposed in #6008.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
| |
| |
| | |
4.02.3 has been the minimal OCaml version for a while now.
|
| |/
|
|
| |
This fixes also #5731, #6035, #5364.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
"_something")
|
| |\ \ \
| | | |
| | | |
| | | | |
BZ#5757)
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
cleared context.
|
| | | | | | |
|
| | | | |/ |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | |
| | | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
|
| | |/
|/|
| |
| |
| |
| | |
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
| |/
|
|
|
|
| |
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This code was probably slightly wrong w.r.t. to a semantics defined as
equivalent to first full-blown normalization followed by kernel term equality.
Or at least, it was adding redundant constraints.
|
| |/
|
|
|
|
|
| |
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| |/ /
| |
| |
| |
| |
| | |
This function is suspicious, and reallocates a lot when it should be the
identity. This matters for detyping, where it is about the only place where
it is used.
|
| | | |
|
| |\ \ |
|
| | | | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
| |\ \ \ \
| |/ / /
|/| | |
| | | | |
the monad.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|_|/
|/| | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Gaëtan Gilbert
Pierre-Marie Pédrot
Matthieu Sozeau
Guillaume Melquiond
Matej Košík