| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
updating Camlp4->Camlp5.
|
|
subdirectory.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
|
|
We also remove some internal implementation details from the mli file,
there due historical reasons.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
