| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
#3125)
|
|\ \
| | |
| | |
| | | |
instance.
|
|\ \ \
| | | |
| | | |
| | | | |
of levels
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
|
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| |_|_|/
|/| | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
subdirectory.
|
|\ \ \ \ \ |
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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).
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| |_|_|/ /
|/| | | |
| | | | |
| | | | | |
This allows us to avoid doing git clean.
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | | |
Calling the test a second time after a make clean was failing due to
an existing "src" directory left by the first call.
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
separator
|
|\ \ \ \ \ |
|
| | | | | | |
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Moving at the same to a passing "env sigma" style rather than passing
"gl". Not that it is strictly necessary, but since we had to move
functions taking only a "sigma" to functions taking also a "env", we
eventually adopted the "env sigma" style. (The "gl" style would have
been as good.)
This answers wish #4717.
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | | |
With help from Guillaume (see discussion at
https://github.com/coq/coq/issues/6191).
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).
They are meant to serve as human-readable sanity checks of output
format.
Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).
N.B. The test-suite removes all *.log files, so we use *.log.in.
N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.
N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| |_|_|_|/ /
|/| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Was broken since 8.6.
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.
To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
(clause "where" with implicit arguments)
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
unbound rel
|
| |_|_|_|_|/ /
|/| | | | | | |
|
| |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This should help debug things like
https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they
ever show up again.
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
local definitions)
|
|\ \ \ \ \ \ \
| |_|_|_|_|/ /
|/| | | | | | |
|
| |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | | |
Fixes #6165.
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
When an evar is undefined we need to substitute inside the evar instance.
With help from @herbelin and @psteckler to identify the issue from a
large test case.
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | | |
|