| Age | Commit message (Collapse) | Author |
|---|
|
Removing in passing two Local which are no-ops in practice.
|
|
This avoid a clash with int_scope in ssreflect's ssrint.v
|
|
This parsing/printing method for nat should be just as fast as
the previous dedicated code. Moreover, we could now parse large
literals as nat numbers, by leaving them in a half-abstract form
such as (Nat.of_uint 123456). This form is convertible to the
closed (S (S (S ...))) form, so it shouldn't be a big deal for
compatibility, except for if some Ltac stuff relies on (S ...) to be
present after parsing. Of course, forcing the computation of
a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
|
|
This way, we could fully bypass bigint.ml.
The previous mechanism of parsing/printing Z is kept for now.
Currently, the conversion functions accepted by Numeral Notation foo
may have the following types.
for parsing:
int -> foo
int -> option foo
uint -> foo
uint -> option foo
Z -> foo
Z -> option foo
for printing:
foo -> int
foo -> option int
foo -> uint
foo -> option uint
foo -> Z
foo -> option Z
Notes:
- The Declare ML Module is directly done in Prelude
- When doing a Numeral Notation, having the Z datatype around
isn't mandatory anymore (but the error messages suggest that
it can still be used).
- An option (abstract after ...) allows to keep large numbers in
an abstract form such as (Nat.of_uint 123456) instead of reducing
to (S (S (S ...))) and ending immediately with Stack Overflow.
- After checking with Matthieu, there is now a explicit check
and an error message in case of polymorphic inductive types
|
|
|
|
|
|
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
|
|
|
|
|
|
|
|
|
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.
We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).
Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.
Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.
Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
|
|
|
|
|
|
Analogous to existing `{x | P}` notation for `sig`, where the type of
`x` is inferred instead of specified.
|
|
|
|
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
|
|
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|
- 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
|
