| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like
`Global Set SsrHave NoTCResolution`. I don't think it is needed (just
let the user write the desired locality), but if it is, the right way of
doing it is to let clients of Goptions specify a default locality.
|
| |
|
|
| |
As stated in the manual, the fourier tactic is subsumed by lra.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
| |\ |
|
| | | |
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| |/ / |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Was revealing a critical bug in VM universe handling introduced in 8.5.
|
| | |/
|/| |
|
| |/ |
|
| | |
|
| |
|
|
|
| |
- we always rename
- we compile {clear}/view to /view{clear}
|
| |
|
|
|
| |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
| |
|
|
|
|
|
| |
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
|
| |
|
|
|
| |
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
| |\ |
|
| |\ \ |
|
| | |/
|/| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
| | | |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Fixes #7243.
|
| | |/
|/| |
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\
| |
| |
| |
| | |
# Conflicts:
# CHANGES
|
| | | |
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| | |
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
| |/
|
|
|
| |
I make here a minimal fix, but a lot of cleaning should be done around
Aux_file handling, including removing some code from the kernel.
|
| |\ |
|
| | | |
|
| |/
|
|
| |
[skip ci]
|
| | |
|
| | |
|
Maxime Dénès
Théo Zimmermann
Vincent Laporte
Pierre-Marie Pédrot
Matthieu Sozeau
Jasper Hugunin
Enrico Tassi
Gaëtan Gilbert
Hugo Herbelin
Emilio Jesus Gallego Arias
Ralf Jung
Jason Gross