| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
functionalization.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
instance.
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| | |_|/
|/| |
| | |
| | |
| | | |
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
| |\ \ \ |
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \
| |_|_|/
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
In particular, we put all the context in the atts structure, and
generalize the type of the parameters of a vernac.
I hope this helps people working on "attributes", my motivation is
indeed having a more robust interpretation.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
We also remove some internal implementation details from the mli file,
there due historical reasons.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | | |
I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
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`.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
|
| | |/
|/|
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
(clause "where" with implicit arguments)
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |/ /
|/| |
| | |
| | |
| | | |
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.
|
| |\ \ |
|
| | | | |
|
| | | | |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Matthieu Sozeau
Hugo Herbelin