| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
As stated in the manual, the fourier tactic is subsumed by lra.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
|
| |
Note that one of them is in the name of the main theorem, so we use a
compatibility notation.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.
Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.
See also #6171.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | | |
This closes #6598
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | |/ / / / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
Analogous to existing `{x | P}` notation for `sig`, where the type of
`x` is inferred instead of specified.
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
.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.
|
| |\ \ \ \ \ |
|
Maxime Dénès
whitequark
Matthieu Sozeau
Hugo Herbelin
Ralf Jung
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Vincent Laporte
Jason Gross
Théo Zimmermann
Pierre Letouzey
Tej Chajed
Ismail
Gaëtan Gilbert
Anton Trunov