[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

@@ -1339,7 +1339,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
@@ -1407,7 +1407,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]
@@ -1550,7 +1550,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

@@ -20,11 +20,11 @@ open Locus
 
 (* Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
-		  rew_type: types;
-		  rew_pat: constr;
-		  rew_ctx: Univ.ContextSet.t;
-		  rew_l2r: bool;
-		  rew_tac: Genarg.glob_generic_argument option }
+                  rew_type: types;
+                  rew_pat: constr;
+                  rew_ctx: Univ.ContextSet.t;
+                  rew_l2r: bool;
+                  rew_tac: Genarg.glob_generic_argument option }
 
 let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
@@ -33,8 +33,8 @@ let subst_hint subst hint =
   let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
-	rew_lemma = cst'; rew_type = typ';
-	rew_pat = pat';	rew_tac = t' }
+        rew_lemma = cst'; rew_type = typ';
+        rew_pat = pat';	rew_tac = t' }
 
 module HintIdent =
 struct
@@ -79,13 +79,13 @@ let print_rewrite_hintdb bas =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   (str "Database " ++ str bas ++ fnl () ++
-	   prlist_with_sep fnl
-	   (fun h ->
-	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
+           prlist_with_sep fnl
+           (fun h ->
+             str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
                Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
-	       Option.cata (fun tac -> str " then use tactic " ++
+               Option.cata (fun tac -> str " then use tactic " ++
                Pputils.pr_glb_generic env sigma tac) (mt ()) h.rew_tac)
-	   (find_rewrites bas))
+           (find_rewrites bas))
 
 type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
 
@@ -116,7 +116,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
     Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
       Tacticals.New.tclTHEN tac
         (Tacticals.New.tclREPEAT_MAIN
-	    (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main)))
+            (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main)))
       (Proofview.tclUNIT()) lrul))
 
 (* The AutoRewrite tactic *)
@@ -125,9 +125,9 @@ let autorewrite ?(conds=Naive) tac_main lbas =
     (List.fold_left (fun tac bas ->
        Tacticals.New.tclTHEN tac
         (one_base (fun dir c tac ->
-	  let tac = (tac, conds) in
-	    general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
-	  tac_main bas))
+          let tac = (tac, conds) in
+            general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
+          tac_main bas))
       (Proofview.tclUNIT()) lbas))
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
@@ -158,19 +158,19 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   else
     let compose_tac t1 t2 =
       match cl.onhyps with
-	| Some [] -> t1
-	| _ ->      Tacticals.New.tclTHENFIRST t1 t2
+        | Some [] -> t1
+        | _ ->      Tacticals.New.tclTHENFIRST t1 t2
     in
     compose_tac
-	(if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ())
-	(match cl.onhyps with
-	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
-	   | None ->
-		 (* try to rewrite in all hypothesis
-		    (except maybe the rewritten one) *)
+        (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ())
+        (match cl.onhyps with
+           | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
+           | None ->
+                 (* try to rewrite in all hypothesis
+                    (except maybe the rewritten one) *)
                Proofview.Goal.enter begin fun gl ->
                  let ids = Tacmach.New.pf_ids_of_hyps gl in
-		 try_do_hyps (fun id -> id)  ids
+                 try_do_hyps (fun id -> id)  ids
                end)
 
 let auto_multi_rewrite ?(conds=Naive) lems cl =
@@ -180,10 +180,10 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
   let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in
   match onconcl,cl.Locus.onhyps with
     | false,Some [_] | true,Some [] | false,Some [] ->
-	(* autorewrite with .... in clause using tac n'est sur que
-	   si clause represente soit le but soit UNE hypothese
-	*)
-	Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
+        (* autorewrite with .... in clause using tac n'est sur que
+           si clause represente soit le but soit UNE hypothese
+        *)
+        Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
     | _ ->
         Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
@@ -233,7 +233,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     let rec split_last_two = function
       | [c1;c2] -> [],(c1, c2)
       | x::y::z ->
-	  let l,res = split_last_two (y::z) in x::l, res
+          let l,res = split_last_two (y::z) in x::l, res
       | _ -> raise Not_found
     in
       try
@@ -255,19 +255,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     match find_rel ctype with
     | Some c -> Some c
     | None ->
-	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' ctx) with
-	| Some c -> Some c
-	| None -> None
+        let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+        match find_rel (it_mkProd_or_LetIn t' ctx) with
+        | Some c -> Some c
+        | None -> None
 
 let find_applied_relation ?loc metas env sigma c left2right =
   let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
-	user_err ?loc ~hdr:"decompose_applied_relation"
-		    (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
-		       spc () ++ str"of this term does not end with an applied relation.")
+        user_err ?loc ~hdr:"decompose_applied_relation"
+                    (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
+                       spc () ++ str"of this term does not end with an applied relation.")
 
 (* To add rewriting rules to a base *)
 let add_rew_rules base lrul =
@@ -279,13 +279,12 @@ let add_rew_rules base lrul =
   let lrul =
     List.fold_left
       (fun dn {CAst.loc;v=((c,ctx),b,t)} ->
-	let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
-	let info = find_applied_relation ?loc false env sigma c b in
-	let pat = if b then info.hyp_left else info.hyp_right in
-	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
-		    rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
-		    rew_tac = Option.map intern t}
-	in incr counter;
-	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
+        let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
+        let info = find_applied_relation ?loc false env sigma c b in
+        let pat = if b then info.hyp_left else info.hyp_right in
+        let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+                    rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
+                    rew_tac = Option.map intern t}
+        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

@@ -28,11 +28,11 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic ->
 
 (** Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
-		  rew_type: types;
-		  rew_pat: constr;
-		  rew_ctx: Univ.ContextSet.t;
-		  rew_l2r: bool;
-		  rew_tac: Genarg.glob_generic_argument option }
+                  rew_type: types;
+                  rew_pat: constr;
+                  rew_ctx: Univ.ContextSet.t;
+                  rew_l2r: bool;
+                  rew_tac: Genarg.glob_generic_argument option }
 
 val find_rewrites : string -> rew_rule list
 
@@ -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

@@ -33,7 +33,7 @@ open Hints
 module NamedDecl = Context.Named.Declaration
 
 (** Hint database named "typeclass_instances", created in prelude *)
-let typeclasses_db = "typeclass_instances"
+let typeclasses_db = Classes.typeclasses_db
 
 (** Options handling *)
 
@@ -457,7 +457,7 @@ let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-let pr_depth l = 
+let pr_depth l =
   let rec fmt elts =
     match elts with
     | [] -> []
@@ -758,8 +758,8 @@ module Search = struct
               Feedback.msg_debug
                 (str"Adding shelved subgoals to the search: " ++
                  prlist_with_sep spc (pr_ev sigma) goals ++
-		 str" while shelving " ++
-		 prlist_with_sep spc (pr_ev sigma) shelved);
+                 str" while shelving " ++
+                 prlist_with_sep spc (pr_ev sigma) shelved);
             shelve_goals shelved <*>
               (if List.is_empty goals then tclUNIT ()
                else
@@ -776,7 +776,7 @@ module Search = struct
              (with_shelf tac >>= fun s ->
               let i = !idx in incr idx; result s i None)
              (fun e' ->
-	      if CErrors.noncritical (fst e') then
+              if CErrors.noncritical (fst e') then
                 (pr_error e'; aux (merge_exceptions e e') tl)
               else iraise e')
     and aux e = function

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/contradiction.ml → plugins/ltac/contradiction.ml

@@ -66,10 +66,10 @@ let contradiction_context =
       | d :: rest ->
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
-	  let typ = whd_all env sigma typ in
+          let typ = whd_all env sigma typ in
           if is_empty_type env sigma typ then
-	    simplest_elim (mkVar id)
-	  else match EConstr.kind sigma typ with
+            simplest_elim (mkVar id)
+          else match EConstr.kind sigma typ with
           | Prod (na,t,u) when is_empty_type env sigma u ->
              let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in
              Tacticals.New.tclORELSE
@@ -84,17 +84,17 @@ let contradiction_context =
                    simplest_elim (mkApp (mkVar id,[|p|]))
                | None ->
                  Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
-	      (Proofview.tclORELSE
+              (Proofview.tclORELSE
                  (Proofview.Goal.enter begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
-	           filter_hyp (fun typ -> is_conv_leq typ t)
-		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
+                   filter_hyp (fun typ -> is_conv_leq typ t)
+                     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                  end)
                  begin function (e, info) -> match e with
-	           | Not_found -> seek_neg rest
+                   | Not_found -> seek_neg rest
                    | e -> Proofview.tclZERO ~info e
                  end)
-	  | _ -> seek_neg rest
+          | _ -> seek_neg rest
     in
     let hyps = Proofview.Goal.hyps gl in
     seek_neg hyps