| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
"rename" flag
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Most of it seems straightforward.
|
| | |_|_|/
|/| | |
| | | |
| | | | |
AFAICT this tactic is always used on ground terms.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|/
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The error is now:
Syntax error: [constr:binder] expected after 'Context' (in [vernac:gallina_ext]).
Close #7452.
|
| | | | | | | | |
|
| | | |_|_|/ /
| |/| | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Close #7562.
[api] move hint_info ast to tactics.
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | | |
|
| | |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | | |
When creating a scheme for bifinite inductive types, we do not create a
fixpoint.
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | | | | | | |
|
| | |/ / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The extension mechanism is specific to metasyntax and vernacinterp,
thus it makes sense to place them next to each other.
We also fix the META entry for the `grammar` camlp5 plugin.
|
| |/ / / /
| | | |
| | | |
| | | | |
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.
|
| |\ \ \
| | | |
| | | |
| | | | |
in CArray
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
I didn't change the parser which expects an integer instead of a positive number
because changing it would also mean having worse error messages because of our
current LL parser. The error message would have been:
Syntax error: 'Tactic' ':=' expected after 'Obligation' (in
[vernac:command]).
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | | |
This API is a bit strange, I expect it will change at some point.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
`comDefinition`.
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
| |/ /
| |
| |
| | |
This should fix #7448 and #7265.
|
| |\ \
| | |
| | |
| | | |
kernel style.
|
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Armaël Guéneau
Hugo Herbelin
Théo Zimmermann