| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | | |
Just because it's fun and easy. Not used by the Numeral Notation command.
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
|
| | | | |
|
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | | |
|
| |/ / /
|/| | |
| | | |
| | | |
| | | | |
.dir-locals led to issues with unsafe local variable warnings. With
this method the user is opting in to running this code so there are no warnings.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ \ \ \ |
|
| | | | | |
|
| | | | | |
|
|/ / / / |
|
| | | | |
|
| |/ /
|/| | |
|
|/ /
| |
| |
| | |
Specifically Exists_dec, Forall_dec, and Forall_Exists_dec.
|
|\ \ |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| | | |
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
| | | |
|
| | | |
|
| | | |
|
|/ / |
|
|\ \
| | |
| | |
| | | |
work better on them
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Rlt_Rpower_l and pow_INR.
Unfortunately theorems Rpower_lt and Rle_power are named inconsistently,
in spite of their similarity.
|
| |/
|/|
| |
| |
| | |
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.
|