[tactics] [rfc] Move ltac-specific tactics to ltac.

This could be seen as a plan to make `tactics` independent of
`vernac`, also it could facilitate the versioning of tactics by
packing them.

Remaining non-core tactics in `tactics` have to remain there due to
scheme declaration. Moving scheme declaration higher would allow us to
move the tactics too.

This PR is a Request for Comments, I am myself not pushing this idea
strongly, feedback welcome. Doing a `Tactics_v8` pack could be another
choice for example.

plugins/funind/functional_principles_proofs.ml

@@ -1340,7 +1340,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 (*               let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
 (*               rewrite *)
 (*            ) *)
-              Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
+              Proofview.V82.of_tactic (Ltac_plugin.Eauto.gen_eauto (false,5) [] (Some []))
             ]
             gls
   | Not_needed -> tclIDTAC
@@ -1408,7 +1408,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
                            (
                             tclCOMPLETE(
                               Proofview.V82.of_tactic @@
-                              Eauto.eauto_with_bases
+                              Ltac_plugin.Eauto.eauto_with_bases
                                 (true,5)
                                 [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
                                 [Hints.Hint_db.empty TransparentState.empty false]
@@ -1551,7 +1551,7 @@ let prove_principle_for_gen
         [
           Proofview.V82.of_tactic (generalize [lemma]);
           Proofview.V82.of_tactic (Simple.intro hid);
-          Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
+          Proofview.V82.of_tactic (Ltac_plugin.Elim.h_decompose_and (mkVar hid));
           (fun g ->
              let new_hyps = pf_ids_of_hyps g in
              tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));

plugins/funind/invfun.ml

@@ -93,7 +93,7 @@ let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl
       ; generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]
       ; clear [hid]
       ; Simple.intro hid
-      ; Inv.inv Inv.FullInversion None (Tactypes.NamedHyp hid)
+      ; Ltac_plugin.Inv.(inv FullInversion None (Tactypes.NamedHyp hid))
       ; Proofview.Goal.enter (fun gl ->
             let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps gl) in
             tclMAP (revert_graph kn pre_tac)  (hid::new_ids)

plugins/funind/recdef.ml

@@ -41,7 +41,7 @@ open Genredexpr
 
 open Equality
 open Auto
-open Eauto
+open Ltac_plugin.Eauto
 
 open Indfun_common
 open Context.Rel.Declaration
@@ -1300,7 +1300,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
             ; Proofview.Goal.enter (fun gl ->
                   let ids = pf_ids_of_hyps gl in
                   tclTHEN
-                    (Elim.h_decompose_and (mkVar hid))
+                    (Ltac_plugin.Elim.h_decompose_and (mkVar hid))
                     (Proofview.Goal.enter (fun gl ->
                          let ids' = pf_ids_of_hyps gl in
                          lid := List.rev (List.subtract Id.equal ids' ids);
@@ -1322,7 +1322,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
                 [ tclTHEN
                     (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
                     e_assumption
-                ; Eauto.eauto_with_bases
+                ; Ltac_plugin.Eauto.eauto_with_bases
                       (true,5)
                       [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
                       [Hints.Hint_db.empty TransparentState.empty false

tactics/autorewrite.ml → plugins/ltac/autorewrite.ml

@@ -288,4 +288,3 @@ let add_rew_rules base lrul =
         in incr counter;
           HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
-

tactics/autorewrite.mli → plugins/ltac/autorewrite.mli

@@ -61,4 +61,3 @@ type hypinfo = {
 val find_applied_relation :
   ?loc:Loc.t -> bool ->
   Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo
-

tactics/class_tactics.ml → plugins/ltac/class_tactics.ml

@@ -32,9 +32,6 @@ open Hints
 
 module NamedDecl = Context.Named.Declaration
 
-(** Hint database named "typeclass_instances", created in prelude *)
-let typeclasses_db = "typeclass_instances"
-
 (** Options handling *)
 
 let typeclasses_debug = ref 0
@@ -986,7 +983,7 @@ module Search = struct
       evars in evd are independent of the rest of the evars *)
 
   let typeclasses_resolve env evd debug depth unique p =
-    let db = searchtable_map typeclasses_db in
+    let db = searchtable_map Classes.typeclasses_db in
     let st = Hint_db.transparent_state db in
     let modes = Hint_db.modes db in
     typeclasses_eauto env evd ?depth unique (modes,st) [db] p
@@ -1144,7 +1141,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in
   let (ev, _) = destEvar sigma t in
   let gls = { it = gl ; sigma = sigma; } in
-  let hints = searchtable_map typeclasses_db in
+  let hints = searchtable_map Classes.typeclasses_db in
   let st = Hint_db.transparent_state hints in
   let modes = Hint_db.modes hints in
   let depth = get_typeclasses_depth () in

tactics/class_tactics.mli → plugins/ltac/class_tactics.mli

@@ -13,8 +13,6 @@
 open Names
 open EConstr
 
-val typeclasses_db : string
-
 val catchable : exn -> bool
 
 val set_typeclasses_debug : bool -> unit

tactics/elim.ml → plugins/ltac/elim.ml

@@ -173,5 +173,3 @@ let double_ind h1 h2 =
   end
 
 let h_double_induction = double_ind
-
-

plugins/ltac/g_class.mlg

@@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto
  | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     { typeclasses_eauto ~depth:d l }
  | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
-     typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
+     typeclasses_eauto ~only_classes:true ~depth:d [Classes.typeclasses_db] }
 END
 
 TACTIC EXTEND head_of_constr

plugins/ltac/ltac_plugin.mlpack

@@ -9,12 +9,21 @@ Tactic_debug
 Tacintern
 Profile_ltac
 Tactic_matching
+Elim
+Inv
+Leminv
 Tacinterp
 Tacentries
 Evar_tactics
 Tactic_option
 Extraargs
 G_obligations
+Contradiction
+Eauto
+Class_tactics
+Term_dnet
+Eqdecide
+Autorewrite
 Coretactics
 Extratactics
 Profile_ltac_tactics

plugins/omega/coq_omega.ml

@@ -28,7 +28,7 @@ open Tactics
 open Logic
 open Libnames
 open Nametab
-open Contradiction
+open Ltac_plugin.Contradiction
 open Tactypes
 open Context.Named.Declaration
 

tactics/tactics.mllib

@@ -16,15 +16,6 @@ Redexpr
 Ppred
 Tactics
 Abstract
-Elim
 Equality
-Contradiction
-Inv
-Leminv
 Hints
 Auto
-Eauto
-Class_tactics
-Term_dnet
-Eqdecide
-Autorewrite

user-contrib/Ltac2/tac2stdlib.ml

@@ -181,16 +181,16 @@ let to_debug v = match Value.to_int v with
 let debug = make_to_repr to_debug
 
 let to_strategy v = match Value.to_int v with
-| 0 -> Class_tactics.Bfs
-| 1 -> Class_tactics.Dfs
+| 0 -> Ltac_plugin.Class_tactics.Bfs
+| 1 -> Ltac_plugin.Class_tactics.Dfs
 | _ -> assert false
 
 let strategy = make_to_repr to_strategy
 
 let to_inversion_kind v = match Value.to_int v with
-| 0 -> Inv.SimpleInversion
-| 1 -> Inv.FullInversion
-| 2 -> Inv.FullInversionClear
+| 0 -> Ltac_plugin.Inv.SimpleInversion
+| 1 -> Ltac_plugin.Inv.FullInversion
+| 2 -> Ltac_plugin.Inv.FullInversionClear
 | _ -> assert false
 
 let inversion_kind = make_to_repr to_inversion_kind
@@ -534,7 +534,7 @@ let () = define_prim3 "tac_injection" bool (option intro_patterns) (option destr
 end
 
 let () = define_prim1 "tac_absurd" constr begin fun c ->
-  Contradiction.absurd c
+  Ltac_plugin.Contradiction.absurd c
 end
 
 let () = define_prim1 "tac_contradiction" (option constr_with_bindings) begin fun c ->

user-contrib/Ltac2/tac2tactics.ml

@@ -372,10 +372,10 @@ let autorewrite ~all by ids cl =
   let ids = List.map Id.to_string ids in
   let cl = mk_clause cl in
   match by with
-  | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
+  | None -> Ltac_plugin.Autorewrite.auto_multi_rewrite ?conds ids cl
   | Some by ->
     let by = thaw Tac2ffi.unit by in
-    Autorewrite.auto_multi_rewrite_with ?conds by ids cl
+    Ltac_plugin.Autorewrite.auto_multi_rewrite_with ?conds by ids cl
 
 (** Auto *)
 
@@ -390,7 +390,7 @@ let auto debug n lems dbs =
   Auto.h_auto ~debug n lems dbs
 
 let new_auto debug n lems dbs =
-  let make_depth n = snd (Eauto.make_dimension n None) in
+  let make_depth n = snd (Ltac_plugin.Eauto.make_dimension n None) in
   let lems = List.map (fun c -> delayed_of_thunk Tac2ffi.constr c) lems in
   match dbs with
   | None -> Auto.new_full_auto ~debug (make_depth n) lems
@@ -401,17 +401,17 @@ let new_auto debug n lems dbs =
 let eauto debug n p lems dbs =
   let lems = List.map (fun c -> delayed_of_thunk Tac2ffi.constr c) lems in
   let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
-  Eauto.gen_eauto (Eauto.make_dimension n p) lems dbs
+  Ltac_plugin.Eauto.gen_eauto (Ltac_plugin.Eauto.make_dimension n p) lems dbs
 
 let typeclasses_eauto strategy depth dbs =
   let only_classes, dbs = match dbs with
   | None ->
-    true, [Class_tactics.typeclasses_db]
+    true, [Classes.typeclasses_db]
   | Some dbs ->
     let dbs = List.map Id.to_string dbs in
     false, dbs
   in
-  Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
+  Ltac_plugin.Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
 (** Inversion *)
 
@@ -431,18 +431,18 @@ let inversion knd arg pat ids =
     begin match arg with
     | None -> assert false
     | Some (_, Tactics.ElimOnAnonHyp n) ->
-      Inv.inv_clause knd pat ids (AnonHyp n)
+      Ltac_plugin.Inv.inv_clause knd pat ids (AnonHyp n)
     | Some (_, Tactics.ElimOnIdent {CAst.v=id}) ->
-      Inv.inv_clause knd pat ids (NamedHyp id)
+      Ltac_plugin.Inv.inv_clause knd pat ids (NamedHyp id)
     | Some (_, Tactics.ElimOnConstr c) ->
       let open Tactypes in
       let anon = CAst.make @@ IntroNaming Namegen.IntroAnonymous in
       Tactics.specialize c (Some anon) >>= fun () ->
-      Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
+      Tacticals.New.onLastHypId (fun id -> Ltac_plugin.Inv.inv_clause knd pat ids (NamedHyp id))
     end
   in
   on_destruction_arg inversion true (Some (None, arg))
 
 let contradiction c =
   let c = Option.map mk_with_bindings c in
-  Contradiction.contradiction c
+  Ltac_plugin.Contradiction.contradiction c

user-contrib/Ltac2/tac2tactics.mli

@@ -116,9 +116,9 @@ val new_auto : Hints.debug -> int option -> constr thunk list ->
 val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
   Id.t list option -> unit Proofview.tactic
 
-val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
+val typeclasses_eauto : Ltac_plugin.Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
-val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
+val inversion : Ltac_plugin.Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic

vernac/classes.ml

@@ -21,13 +21,14 @@ open Globnames
 open Constrintern
 open Constrexpr
 open Context.Rel.Declaration
-open Class_tactics
 open Libobject
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 (*i*)
 
+let typeclasses_db = "typeclass_instances"
+
 let set_typeclass_transparency c local b =
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))

vernac/classes.mli

@@ -14,6 +14,9 @@ open Constrexpr
 open Typeclasses
 open Libnames
 
+(** Hint database named "typeclass_instances", created in prelude *)
+val typeclasses_db : string
+
 (** Instance declaration *)
 
 val declare_instance : ?warn:bool -> env -> Evd.evar_map ->