| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
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.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
|/
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|\ |
|
|\ \ |
|
| | | |
|
| |/
|/|
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
|/
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
|
|
|
| |
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
|
| |
|
|
|
|
| |
This is for eventually being reused in Ltac messages ("idtac").
|
| |
|
|\ |
|
| |
| |
| |
| |
| | |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|/ |
|
| |
|
|
|
|
|
|
|
|
|
| |
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
| |
|
|
|
|
|
| |
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
|/
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
|\ |
|
|\ \ |
|
| | | |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
|/ |
|
|\
| |
| |
| | |
top of the linking chain.
|
|\ \ |
|
| | | |
|
|/ /
| |
| |
| |
| | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
|/
|
|
| |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
|\
| |
| |
| | |
restructuration
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
| |/ /
|/| |
| | |
| | | |
This was already the case, but the API was not exposing this.
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
|\ \ \ \
| |_|/ /
|/| | | |
|
| | | | |
|
| |/ / |
|