| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Fix new deprecation warnings in the standard library.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
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.
|
Maxime Dénès
Théo Zimmermann
Vincent Laporte
Pierre Letouzey
Hugo Herbelin
Ismail
Gaëtan Gilbert
Jason Gross
Jasper Hugunin
Jasper Hugunin
Joachim Breitner
fredokun
Tej Chajed
Raphaël Monat
Emilio Jesus Gallego Arias
Yves Bertot