| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
This fixes #6286 as suggested by PMP. See details of discussion at #6286.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
| | | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|/ / / / / |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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).
|
|/ / / / |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We generalize the possible use of levels to raw and glob printers.
This is potentially useful for printing ltac expressions which are the
glob level.
|
| |_|/
|/| |
| | |
| | |
| | | |
The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
constructs.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
|\ \ \ \ \ \ \
| |_|_|/ / / /
|/| | | | | | |
|
| | | | | | | |
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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).
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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 mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| |/ /
|/| |
| | |
| | |
| | |
| | | |
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.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | | |
Was broken since 8.6.
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
in make.
|
| |_|_|_|/ /
|/| | | | | |
|
| |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ \ \ \ |
|
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| |_|/ /
|/| | |
| | | |
| | | | |
Mismatch probably caused by c5aca4005.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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".
|