Remove the implicit tactic feature following #7229.

15 files changed, 20 insertions, 135 deletions

diff --git a/CHANGES.md b/CHANGES.md
index e280cc2fb5..253f14e9b0 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -67,6 +67,8 @@ Vernacular commands
 - Binders for an `Instance` now act more like binders for a `Theorem`.
   Names may not be repeated, and may not overlap with section variable names.
 
+- Removed the deprecated `Implicit Tactic` family of commands.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
new file mode 100644
index 0000000000..4536c62c64
--- /dev/null
+++ b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=rm-implicit-tactic
+
+if [ "$CI_PULL_REQUEST" = "8779" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    ltac2_CI_REF="$_OVERLAY_BRANCH"
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 9dae7fd102..3ddfc9aec1 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2247,7 +2247,3 @@ expression as described in :ref:`ltac`.
 This construction is useful when one wants to define complicated terms
 using highly automated tactics without resorting to writing the proof-term
 by means of the interactive proof engine.
-
-This mechanism is comparable to the ``Declare Implicit Tactic`` command
-defined at :ref:`tactics-implicit-automation`, except that the used
-tactic is local to each hole instead of being declared globally.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 457f9b2efa..041f1bc966 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3745,32 +3745,6 @@ Setting implicit automation tactics
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   .. cmd:: Declare Implicit Tactic @tactic
-
-      This command declares a tactic to be used to solve implicit arguments
-      that Coq does not know how to solve by unification. It is used every
-      time the term argument of a tactic has one of its holes not fully
-      resolved.
-
-      .. deprecated:: 8.9
-
-         This command is deprecated. Use :ref:`typeclasses <typeclasses>` or
-         :ref:`tactics-in-terms <tactics-in-terms>` instead.
-
-      .. example::
-
-         .. coqtop:: all
-
-            Parameter quo : nat -> forall n:nat, n<>0 -> nat.
-            Notation "x // y" := (quo x y _) (at level 40).
-            Declare Implicit Tactic assumption.
-            Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
-            intros.
-            exists (n // m).
-
-         The tactic ``exists (n // m)`` did not fail. The hole was solved
-         by ``assumption`` so that it behaved as ``exists (quo n m H)``.
-
 .. _decisionprocedures:
 
 Decision procedures
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 85fb0c73c9..70e5ab38bc 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -48,7 +48,6 @@ let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
  } in
@@ -343,7 +342,6 @@ open Vars
 let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
-  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
@@ -571,44 +569,6 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
     { add_transitivity_lemma false t }
 END
 
-{
-
-let cache_implicit_tactic (_,tac) = match tac with
-  | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
-  | None -> Pfedit.clear_implicit_tactic ()
-
-let subst_implicit_tactic (subst,tac) =
-  Option.map (Tacsubst.subst_tactic subst) tac
-
-let inImplicitTactic : glob_tactic_expr option -> obj =
-  declare_object {(default_object "IMPLICIT-TACTIC") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o);
-       cache_function = cache_implicit_tactic;
-       subst_function = subst_implicit_tactic;
-       classify_function = (fun o -> Dispose)}
-
-let warn_deprecated_implicit_tactic =
-  CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated"
-    (fun () -> strbrk "Implicit tactics are deprecated")
-
-let declare_implicit_tactic tac =
-  let () = warn_deprecated_implicit_tactic () in
-  Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac)))
-
-let clear_implicit_tactic () =
-  let () = warn_deprecated_implicit_tactic () in
-  Lib.add_anonymous_leaf (inImplicitTactic None)
-
-}
-
-VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac }
-| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () }
-END
-
-
-
-
 (**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 5af393a3e5..7be8f67616 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -55,7 +55,6 @@ let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2a046a3e65..5bfb0f79fb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -543,7 +543,6 @@ let interp_gen kind ist pattern_mode flags env sigma c =
 let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
@@ -558,21 +557,18 @@ let interp_type = interp_constr_gen IsType
 let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = None;
   fail_evar = false;
   expand_evars = false }
 
@@ -987,7 +983,7 @@ let rec read_match_rule lfun ist env sigma = function
   | [] -> []
 
 (* Fully evaluate an untyped constr *)
-let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+let type_uconstr ?(flags = (constr_flags ()))
   ?(expected_type = WithoutTypeConstraint) ist c =
   begin fun env sigma ->
   let { closure; term } = c in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index be8f3603e4..ddfd4c101f 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -242,7 +242,6 @@ let interp_refine ist gl rc =
   let flags = {
     Pretyping.use_typeclasses = true;
     solve_unification_constraints = true;
-    use_hook = None;
     fail_evar = false;
     expand_evars = true }
   in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cba1533da5..8c57fc2375 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -193,7 +193,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
-  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
@@ -247,14 +246,14 @@ let apply_typeclasses env sigma frozen fail_evar =
     else sigma in
   sigma
 
-let apply_inference_hook hook sigma frozen = match frozen with
+let apply_inference_hook hook env sigma frozen = match frozen with
 | FrozenId _ -> sigma
 | FrozenProgress (lazy (_, pending)) ->
   Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
       try
-        let sigma, c = hook sigma evk in
+        let sigma, c = hook env sigma evk in
         Evd.define evk c sigma
       with Exit ->
         sigma
@@ -307,16 +306,16 @@ let check_evars_are_solved env sigma frozen =
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
-let solve_remaining_evars flags env sigma init_sigma =
+let solve_remaining_evars ?hook flags env sigma init_sigma =
   let frozen = frozen_and_pending_holes (init_sigma, sigma) in
   let sigma =
     if flags.use_typeclasses
     then apply_typeclasses env sigma frozen false
     else sigma
   in
-  let sigma = if Option.has_some flags.use_hook
-    then apply_inference_hook (Option.get flags.use_hook env) sigma frozen
-    else sigma
+  let sigma = match hook with
+  | None -> sigma
+  | Some hook -> apply_inference_hook hook env sigma frozen
   in
   let sigma = if flags.solve_unification_constraints
     then apply_heuristics env sigma false
@@ -1075,14 +1074,12 @@ let ise_pretype_gen flags env sigma lvar kind c =
 let default_inference_flags fail = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = None;
   fail_evar = fail;
   expand_evars = true }
 
 let no_classes_no_fail_inference_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = None;
   fail_evar = false;
   expand_evars = true }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 0f95d27528..2eaa77b822 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -35,7 +35,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
-  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
@@ -95,7 +94,7 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
 
-val solve_remaining_evars : inference_flags ->
+val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
   env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
 
 (** Checking evars and pending conversion problems are all solved,
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index c80f370fdc..cb71f09826 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -53,7 +53,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     let flags = {
       Pretyping.use_typeclasses = true;
       Pretyping.solve_unification_constraints = true;
-      Pretyping.use_hook = None;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e6507332b1..7b55941874 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -227,36 +227,3 @@ let refine_by_tactic env sigma ty tac =
       this hack will work in most cases. *)
   let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
-
-(**********************************************************************)
-(* Support for resolution of evars in tactic interpretation, including
-   resolution by application of tactics *)
-
-let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
-
-let declare_implicit_tactic tac = implicit_tactic := Some tac
-
-let clear_implicit_tactic () = implicit_tactic := None
-
-let apply_implicit_tactic tac = (); fun env sigma evk ->
-  let evi = Evd.find_undefined sigma evk in
-  match snd (evar_source evk sigma) with
-  | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
-      when
-	Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
-	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
-      (try
-        let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in
-        let c = EConstr.of_constr c in
-        if Evarutil.has_undefined_evars sigma c then raise Exit;
-        let (ans, _, ctx) =
-	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
-        let sigma = Evd.set_universe_context sigma ctx in
-        sigma, EConstr.of_constr ans
-       with e when Logic.catchable_exception e -> raise Exit)
-  | _ -> raise Exit
-
-let solve_by_implicit_tactic () = match !implicit_tactic with
-| None -> None
-| Some tac -> Some (apply_implicit_tactic tac)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5feb5bd645..50ce267c81 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -116,13 +116,3 @@ val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.ta
     evars solved by side-effects are NOT purged, so that unexpected failures may
     occur. Ideally all code using this function should be rewritten in the
     monad. *)
-
-(** Declare the default tactic to fill implicit arguments *)
-
-val declare_implicit_tactic : unit Proofview.tactic -> unit
-
-(** To remove the default tactic *)
-val clear_implicit_tactic : unit -> unit
-
-(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1646906daa..03ad1b4c4f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1152,7 +1152,6 @@ let rec intros_move = function
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3b041b7065..d537436c6b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -418,8 +418,8 @@ let start_proof_com ?inference_hook kind thms hook =
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
     let flags = all_and_fail_flags in
-    let flags = { flags with use_hook = inference_hook } in
-    let evd = solve_remaining_evars flags env evd Evd.empty in
+    let hook = inference_hook in
+    let evd = solve_remaining_evars ?hook flags env evd Evd.empty in
     let ids = List.map RelDecl.get_name ctx in
     check_name_freshness (pi1 kind) id;
     (* XXX: The nf_evar is critical !! *)