[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, 3 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0499ba200e..5fb519cc4f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -878,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Declare.declare_universe_context ~poly:false ctx;
+      DeclareUctx.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
@@ -1437,8 +1437,7 @@ let pr_hint_term env sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Declare.Proof.get_proof pf in
-  let Proof.{goals;sigma} = Proof.data pts in
+  let Proof.{goals;sigma} = Proof.data pf in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->