From ad6d5a658806d1c0cf46a39f58113bfbd2ac808d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Oct 2018 15:10:29 +0200 Subject: Remove the implicit tactic feature following #7229. --- CHANGES.md | 2 ++ .../08779-ppedrot-rm-implicit-tactic.sh | 8 +++++ doc/sphinx/language/gallina-extensions.rst | 4 --- doc/sphinx/proof-engine/tactics.rst | 26 -------------- plugins/ltac/extratactics.mlg | 40 ---------------------- plugins/ltac/g_auto.mlg | 1 - plugins/ltac/tacinterp.ml | 6 +--- plugins/ssr/ssrcommon.ml | 1 - pretyping/pretyping.ml | 15 ++++---- pretyping/pretyping.mli | 3 +- proofs/evar_refiner.ml | 1 - proofs/pfedit.ml | 33 ------------------ proofs/pfedit.mli | 10 ------ tactics/tactics.ml | 1 - vernac/lemmas.ml | 4 +-- 15 files changed, 20 insertions(+), 135 deletions(-) create mode 100644 dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh 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 ` or - :ref:`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 !! *) -- cgit v1.2.3