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

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 43e86fa9bd..776ffd6b9f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -91,7 +91,7 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
   let () = match scope with
     | Discharge ->
       (* declare universes separately for variables *)
-      Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+      DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
     | Global _ -> ()
   in
   let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
@@ -191,7 +191,7 @@ let context_subst subst (name,b,t,impl) =
 
 let context_insection sigma ~poly ctx =
   let uctx = Evd.universe_context_set sigma in
-  let () = Declare.declare_universe_context ~poly uctx in
+  let () = DeclareUctx.declare_universe_context ~poly uctx in
   let fn subst (name,_,_,_ as d) =
     let d = context_subst subst d in
     let () = match d with
@@ -226,7 +226,7 @@ let context_nosection sigma ~poly ctx =
       (* Multiple monomorphic axioms: declare universes separately to
          avoid redeclaring them. *)
       let uctx = Evd.universe_context_set sigma in
-      let () = Declare.declare_universe_context ~poly uctx in
+      let () = DeclareUctx.declare_universe_context ~poly uctx in
       Monomorphic_entry Univ.ContextSet.empty
   in
   let fn subst d =