[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 coq#10951 for now and helps with coq#11492 .

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

plugins/ltac/extratactics.mlg

@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
         else (* This is a global universe context that shouldn't be
                 refreshed at every use of the hint, declare it globally. *)
-          (Declare.declare_universe_context ~poly:false ctx;
+          (DeclareUctx.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in

plugins/ltac/ltac_plugin.mlpack

@@ -9,6 +9,7 @@ Tactic_debug
 Tacintern
 Profile_ltac
 Tactic_matching
+Leminv
 Tacinterp
 Tacentries
 Evar_tactics

plugins/setoid_ring/newring.ml

@@ -150,7 +150,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
-  let () = Declare.declare_universe_context ~poly:false univs in
+  let () = DeclareUctx.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant ~name:(Id.of_string na)

tactics/abstract.ml

@@ -40,6 +40,9 @@ let name_op_to_name ~name_op ~name suffix =
   | Some s -> s
   | None -> Nameops.add_suffix name suffix
 
+let declare_abstract = ref (fun ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl ->
+  CErrors.anomaly (Pp.str "Abstract declaration hook not registered"))
+
 let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
@@ -77,7 +80,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let concl = it_mkNamedProd_or_LetIn concl sign in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let effs, sigma, lem, args, safe =
-    Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
+    !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args

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

tactics/declareUctx.ml

@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Monomorphic universes need to survive sections. *)
+
+let name_instance inst =
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Names.Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
+        Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
+let declare_universe_context ~poly ctx =
+  if poly then
+    let uctx = Univ.ContextSet.to_context ctx in
+    let nas = name_instance (Univ.UContext.instance uctx) in
+    Global.push_section_context (nas, uctx)
+  else
+    Global.push_context_set ~strict:true ctx

tactics/declareUctx.mli

@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit

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::_ ->

tactics/hints.mli

@@ -288,7 +288,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Declare.Proof.t -> Pp.t
+val pr_applicable_hint : Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t

tactics/ind_tables.ml

@@ -86,15 +86,15 @@ let compute_name internal id =
     Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
   else id
 
+let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
+    CErrors.anomaly (Pp.str "scheme declaration not registered"))
+
 let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = Declare.pure_definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
-  let () = if internal then () else Declare.definition_message id in
-  kn, eff
+  !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let (c, ctx), eff = f mode ind in

tactics/ind_tables.mli

@@ -59,3 +59,11 @@ val check_scheme : 'a scheme_kind -> inductive -> bool
 val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
 
 val pr_scheme_kind : 'a scheme_kind -> Pp.t
+
+val declare_definition_scheme :
+  (internal : bool
+   -> univs:Entries.universes_entry
+   -> role:Evd.side_effect_role
+   -> name:Id.t
+   -> Constr.t
+   -> Constant.t * Evd.side_effects) ref

tactics/tactics.mllib

@@ -1,5 +1,4 @@
 DeclareScheme
-Declare
 Dnet
 Dn
 Btermdn
@@ -18,7 +17,7 @@ Elim
 Equality
 Contradiction
 Inv
-Leminv
+DeclareUctx
 Hints
 Auto
 Eauto

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 =

vernac/comHints.ml

@@ -97,7 +97,7 @@ let interp_hints ~poly h =
     let c, diff = Hints.prepare_hint true env sigma (evd, c) in
     if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
     else
-      let () = Declare.declare_universe_context ~poly:false diff in
+      let () = DeclareUctx.declare_universe_context ~poly:false diff in
       (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
   in
   let fref r =

tactics/declare.ml → vernac/declare.ml

@@ -133,31 +133,6 @@ let _ = CErrors.register_handler (function
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
-(** Monomorphic universes need to survive sections. *)
-
-let name_instance inst =
-  let map lvl = match Univ.Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        Name (Libnames.qualid_basename qid)
-      with Not_found ->
-        (* Best-effort naming from the string representation of the level.
-           See univNames.ml for a similar hack. *)
-        Name (Id.of_string_soft (Univ.Level.to_string lvl))
-  in
-  Array.map map (Univ.Instance.to_array inst)
-
-let declare_universe_context ~poly ctx =
-  if poly then
-    let uctx = Univ.ContextSet.to_context ctx in
-    let nas = name_instance (Univ.UContext.instance uctx) in
-    Global.push_section_context (nas, uctx)
-  else
-    Global.push_context_set ~strict:true ctx
-
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -589,7 +564,7 @@ let declare_variable ~name ~kind d =
       let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
-      let () = declare_universe_context ~poly univs in
+      let () = DeclareUctx.declare_universe_context ~poly univs in
       let se = {
         Entries.secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
@@ -899,3 +874,13 @@ module Proof = struct
   let update_global_env = update_global_env
   let get_open_goals = get_open_goals
 end
+
+let declare_definition_scheme ~internal ~univs ~role ~name c =
+  let kind = Decls.(IsDefinition Scheme) in
+  let entry = pure_definition_entry ~univs c in
+  let kn, eff = declare_private_constant ~role ~kind ~name entry in
+  let () = if internal then () else definition_message name in
+  kn, eff
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := declare_abstract

tactics/declare.mli → vernac/declare.mli

@@ -135,8 +135,6 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
@@ -262,19 +260,6 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
     Returns [false] if an unsafe tactic has been used. *)
 val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
 
-(** Declare abstract constant; will check no evars are possible; *)
-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
-
 val build_by_tactic
   :  ?side_eff:bool
   -> Environ.env

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

vernac/vernac.mllib

@@ -9,6 +9,7 @@ Himsg
 Locality
 Egramml
 Vernacextend
+Declare
 ComHints
 Ppvernac
 Proof_using

vernac/vernacentries.ml

@@ -1719,7 +1719,8 @@ let vernac_print ~pstate ~atts =
   | PrintHintGoal ->
      begin match pstate with
      | Some pstate ->
-       Hints.pr_applicable_hint pstate
+       let pf = Declare.Proof.get_proof pstate in
+       Hints.pr_applicable_hint pf
      | None ->
        str "No proof in progress"
      end