| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
| | |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
updating Camlp4->Camlp5.
|
|\ \ \ \ \ \
| |_|_|_|_|/
|/| | | | |
| | | | | | |
subdirectory.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Also nicer error when the constraints are impossible.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
This fixes BZ#5717.
Also add a test and fix a changed test.
|
| | | | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
We also remove some internal implementation details from the mli file,
there due historical reasons.
|
| |_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
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.
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Before sometimes there were lists and strings.
|
| |_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
constructs.
|
| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
This allows us to avoid doing git clean.
|
| |_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Fixes #6120.
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Hopefully this will stop the intermittent
test-suite/coq-makefile/findlib-package failures.
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Calling the test a second time after a make clean was failing due to
an existing "src" directory left by the first call.
|