[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, 2 insertions, 2 deletions

diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 20fa43c8e7..89f3503f4d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -94,7 +94,7 @@ let do_universe ~poly l =
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  Declare.declare_universe_context ~poly ctx
+  DeclareUctx.declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
   let open Univ in
@@ -107,4 +107,4 @@ let do_constraint ~poly l =
       Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  Declare.declare_universe_context ~poly uctx
+  DeclareUctx.declare_universe_context ~poly uctx