| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
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.
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
global proof.
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
As a bonus we remove some trailing whitespace, and implement a couple
of hints suggested in the discussion.
|
|/ / / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Was broken since 8.6.
|
| |_|_|_|_|_|_|_|_|/
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Replaced by ident_decl in #688.
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
feature.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
in make.
|
| | | | | | | | | |_|_|_|_|/ /
| | | | | | | | |/| | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
(clause "where" with implicit arguments)
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
unbound rel
|
| |_|_|_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Fixes #4988.
|
| |_|_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
| |_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
We require 4.02.3.
|
| |_|_|_|_|_|/ / / / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
While we are at it we refactor a few special cases of the helper.
|
| |_|_|_|_|/ / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
As of Nov 2017, the standard number of entries is 85, it easily goes
up with some other plugins, so 211 seems like a good compromise.
|
| |_|_|_|_|_|_|/ /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
| |_|_|_|_|_|/ /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This should help debug things like
https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they
ever show up again.
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
local definitions)
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Mismatch probably caused by c5aca4005.
|
| |_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Fixes #6165.
|
| |_|_|_|_|_|_|/ / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The warning created problems as OCaml restored the color printing tags
when printing it, so users doing `Drop` and then `go ()` got color
printing back after the warning.
We should guard the console on `Drop` better, but this requires some
(much needed) refactoring work in the toplevel.
|
| |_|_|_|/ / / / /
|/| | | | | | | | |
|
| |_|_|_|/ / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We preserve the level instead of resetting it at level 0.
Probably it would be the same as giving level ltop since Tacexp
apparently comes only from using a tactic in an Ltac "let", which is
where I observed a problem.
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This is to avoid excessive parentheses, in particular when printing
"constr:()" in "Print Ltac f".
|
|\ \ \ \ \ \ \ |
|