Remove the implicit tactic feature following #7229.

3 files changed, 0 insertions, 44 deletions

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