diff options
| author | Emilio Jesus Gallego Arias | 2020-04-18 22:58:40 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:12 +0200 |
| commit | e04377e2c5eca2b47bd5f8db320069aa47040488 (patch) | |
| tree | 920a54578946602f6f51b106b534a534ec8068c8 /dev/base_include | |
| parent | 688a0869f6b8ab3048a545f821f45bc5599ba63b (diff) | |
[declare] [tactics] Move declare to `vernac`
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 96a867475d..45e79147c1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -129,7 +129,7 @@ open Elim open Equality open Hipattern open Inv -open Leminv +open Ltac_plugin.Leminv open Tacticals open Tactics open Eqschemes |