| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
| | | |
|
| | |
| |
| |
| | |
The concrete syntax is still restricted to identifiers.
|
| | | |
|
| | | |
|
| | | |
|
| |/
|
|
| |
Elaborate a [atts] record out of a list of flags.
|
| | |
|
| |
|
|
| |
Don't allow notations attached to uniform inductives
|
| | |
|
| |
|
|
| |
Highly spaghetti code, hopefully works.
|
| |
|
|
|
|
|
|
| |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| |
|
|
| |
We move the last 3 types to more adequate places.
|
| |\
| |
| |
| | |
"rename" flag
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| | |/ / |
|
| |/ /
| |
| |
| | |
We address the easy ones, but they should probably be all removed.
|
| |/
|
|
|
| |
Using a formulation which makes it is clear that no renaming has been
done. See discussion at issue #2987.
|
| |
|
|
|
|
| |
There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
|
| |
|
|
|
|
|
| |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
| |\ |
|
| | |
| |
| |
| |
| | |
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
| |/
|
|
| |
This API is a bit strange, I expect it will change at some point.
|
| |
|
|
|
|
|
|
|
|
| |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | | |
Normalization sounds like it should be semantically noop.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| | |
Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].
The fix is fortunately easy.
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.
|
| |/ / |
|
| | | |
|
| | | |
|
| |/
|
|
|
|
| |
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| |
|
|
|
|
|
| |
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
|
| |
|
|
| |
This prevents relying on an underspecified bool option argument.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| | |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Vincent Laporte
Jasper Hugunin
Gaëtan Gilbert
Maxime Dénès
Hugo Herbelin
Enrico Tassi