| Commit message (Collapse) | Author | Age |
... | |
| |_|_|/ /
|/| | | | |
|
| | | | | |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |/ / / / /
|/| | | | | |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | | |
Was still relying on the existence of user-configured /pr/.
|
| | | |/ /
| | |/| |
| | | | |
| | | | |
| | | | | |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| |_|_|/
|/| | | |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove the progs target [examples] to save time, we still build the
full library thou.
I guess we can't do better for now unless we get some Travis
subscription.
|
|\ \ \ |
|
| |/ / |
|
|\ \ \ |
|
|\ \ \ \
| |_|/ /
|/| | | |
|
| | | | |
|
|\ \ \ \
| |_|_|/
|/| | | |
|
| |/ /
|/| |
| | |
| | |
| | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
| |_|_|/
|/| | | |
|
| |_|/
|/| | |
|
|\ \ \ |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
|/|
| |
| |
| |
| | |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
|\ \ \ \ |
|
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| |_|/ /
|/| | | |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
|/ |
|
|\ |
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
type is unknown
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | | |
It made the test always fail so ci-common was always sourced. It's not
quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Actually, ocaml is apparently doing well. If there is a printer for 'a
Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined
existing ones, so, it is apparently not a problem to have overlapping
printer.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| |_|_|_|/ /
|/| | | | | |
|