| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
The real list is computed by tok_using in CLexer.
|
|
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.
Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
|
|
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef
|
|
Note that this slightly changes the semantics of backtracking across
`start ltac profiling`.
|
|
Fixes #12196
|
|
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
|
|
|
|
Reviewed-by: ppedrot
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
