| Commit message (Collapse) | Author | Age |
... | |
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
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.
|
| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
The primary concern is for clarity of reading.
May it affects tools which would parse the output of "Print LoadPath"?
Presumably, these tools would not support file names with spaces
already, so this may have no impact.
|
| | | | | | | | | | | | |
|
| |_|_|_|_|_|/ / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Was actually forgotten in native-coq.
|
| | | | |_|_|_|_|/ /
| | | |/| | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
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).
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Making it bigger is kind of useless, takes time and clutters the output for
no real advantage.
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
| |_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
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)
|
| |_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Previously, it was reverse-ordering timing diffs.
|
| |_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Note the problem with `create_evar_defs`.
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
With a bit of care we can enable full deprecation warnings again in
this funny file.
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|