| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
work better on them
|
| |
| |
| |
| |
| | |
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
|/ |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
| |_|/
|/| | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an
unexpected extra dependency due to a name collision with a section
variable.
|
| |/
|/|
| |
| | |
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
|
| | |
|
| | |
|
| | |
|
|/ |
|
|\ |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| | |
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607).
PR #220 put the exports in the wrong compat files, presumably because it
was originally targeted to version 8.6, and this wasn't updated when it
was retargeted to version 8.7.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | |
| | |
| | | |
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
| | | |
|
| |/
|/| |
|
| |
| |
| |
| | |
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.
|