| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
| |
| |
| |
| | |
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]
|
| |
|
| |
|
|\
| |
| |
| | |
deciding…
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
notation to use among several of them"
This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
|
|\ \ \
| |_|/
|/| | |
|
| | | |
|
|\ \ \
| |_|/
|/| | |
|
|\ \ \ |
|
| |_|/
|/| | |
|
| |/
|/| |
|
|\ \
| | |
| | |
| | | |
fiat-crypto/OSX
|
|\ \ \
| | | |
| | | |
| | | | |
wish #4129)
|