| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
|
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
|
|
|
|
|
|
|
|
|
|
| |
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
| |
|
| |
|
| |
|
| |
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|