| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|
|
|
| |
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
(for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
- wrong -for-pack used for their inner .cmx
- dependency over modules not provided (for instance Tacenv, that ends
up being a submodule of the pack ltac_plugin).
But we were lucky, those files were actually never loaded, thanks to the
several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
and hence tell Coq that these modules are already known, preventing
any attempt to load them.
Anyway, this commit cleans up this mess (thanks PMP for the help)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
|\ |
|
| |
| |
| |
| | |
automatically instead
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
| |
| |
| |
| |
| | |
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
| |
| |
| |
| |
| | |
Forwards/backwards reasoning thoughts come from
https://github.com/coq/coq/pull/385#discussion_r111008347
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ' was originally denoting that we were taking in the projections and
applying the constructor in the conclusion, rather than taking in the
bundled versions and projecting them out (because the projections don't
exist for [ex] and [ex2]). But we don't have versions like this for
[sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the
' to the [ex] and [ex2] versions.
|
| |
| |
| |
| | |
As per Hugo's request.
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
As per Hugo's suggestion in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
| |
| |
| |
| | |
This tactic does better than [inversion] at sigma types.
|
| | |
|
| |
| |
| |
| | |
As per Hugo's request.
|
| |
| |
| |
| |
| | |
As per Hugo's request in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
|/ |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The dependent induction tactic notation is in the standard library but
not loaded by default, leading to a parser error message that is
confusing and unhelpful. This commit adds a notation for dependent
induction to Init that fails and reports [Require Import
Coq.Program.Equality.] is required to use [dependent induction].
|
| |/ / |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
These set up PG to use the local coqtop, and the local coqlib, when
editing files in the stdlib. As per
https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use
`_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those
files. However, we cannot use it for `theories/`, because a
`_CoqProject` file will override a `.dir-locals.el` in the same
directory, and there is no way to get PG to pick up a valid `-coqlib`
from `_CoqProject` (because it'll take the path relative to the current
directory, not relative to the directory of `_CoqProject`).
|
|\ \ |
|
| | | |
|
| |/
|/| |
|
|/
|
| |
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
|\ |
|
|\ \ |
|
| | |\
| | | |
| | | |
| | | | |
Was needed to be done for a while.
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Don't know if compare_cont is very useful to use, but, at least, these
extensions make sense.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This completes the series and cannot hurt.
|
| | | | | |
|
|/ / / / |
|