[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 .

1 files changed, 12 insertions, 0 deletions

diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 5c936ff9d6..a138a457b3 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,15 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val declare_abstract :
+  (  name:Names.Id.t
+  -> poly:bool
+  -> kind:Decls.logical_kind
+  -> sign:EConstr.named_context
+  -> secsign:Environ.named_context_val
+  -> opaque:bool
+  -> solve_tac:unit Proofview.tactic
+  -> Evd.evar_map
+  -> EConstr.t
+  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) ref