diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d6391d9941d325a526ab96c62f12fbcd4545d3a..96e4c1696f4d2667fea0680e38c284fac541a521 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,8 +7,6 @@ API-breaking change is listed. - Add lemma `lookup_total_fmap`. - Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`, `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel) -- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but - automatically adds `_` until the given lemma takes no more arguments. - Rename `map_filter_empty_iff` to `map_empty_filter` and add `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler) - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`: diff --git a/stdpp/tactics.v b/stdpp/tactics.v index a7e8552d27c11ec85ab757837f2e83ca232dbd10..f3a30dc5b131b0ea8f9fc4395c12aeb2548da96f 100644 --- a/stdpp/tactics.v +++ b/stdpp/tactics.v @@ -738,19 +738,6 @@ Tactic Notation "ospecialize" "*" uconstr(p) := pose proof p as H'; clear H; rename H' into H )). -(** Tactic that works like [notypeclasses refine] but automatically determines -the right number of [_]. This is *not* goal-directed, it will add [_] until the -given term no longer has a function type (determined without any unfolding). *) -Tactic Notation "notypeclasses" "apply" uconstr(p) := - opose_core p ltac:(fun p => evar_foralls p () ltac:(fun t => t) - ltac:(fun p => notypeclasses refine p || - let T := type of p in - lazymatch goal with |- ?G => - fail "the given term has type" T "while it is expected to have type" G - end - ) - ). - (** The block definitions are taken from [Coq.Program.Equality] and can be used by tactics to separate their goal from hypotheses they generalize over. *) Definition block {A : Type} (a : A) := a. diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v index 36a1b7381ca5eb2aaa9ae2bce99e002131cf7ec7..af70961286cb48cc4ca2f3bd97377ac794941dca 100644 --- a/stdpp_bitvector/definitions.v +++ b/stdpp_bitvector/definitions.v @@ -755,7 +755,7 @@ Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db. tries to simplify them by removing any [bv_wrap] inside z1. *) Ltac bv_wrap_simplify_left := lazymatch goal with |- bv_wrap _ _ = _ => idtac end; - etrans; [ notypeclasses apply bv_wrap_simplify_proof; + etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _); typeclasses eauto with bv_wrap_simplify_db | ] . diff --git a/tests/tactics.ref b/tests/tactics.ref index 5bf23c455d37cdfdeeaa6e84e6d5440577e9ff67..ab5fadcfbbe399c27857691818027eb6d68dac2b 100644 --- a/tests/tactics.ref +++ b/tests/tactics.ref @@ -65,22 +65,9 @@ use opose proof instead. H' : even n ============================ even n -"notypeclasses_apply_test" - : string -1 goal - - n : nat - ============================ - Decision (n = 0) -1 goal - - n : nat - ============================ - Decision (n = 0) "notypeclasses_apply_error" : string The command has indeed failed with message: -Tactic failure: the given term has type Q while it is expected to have type -P. +The reference notypeclasses was not found in the current environment. The command has indeed failed with message: No such assumption. diff --git a/tests/tactics.v b/tests/tactics.v index 990bccb0da95a279a624d79ccf1395cf3d4cf595..7e7271b3bb4a60bfc68003d433238e80a5f86095 100644 --- a/tests/tactics.v +++ b/tests/tactics.v @@ -234,16 +234,6 @@ Proof. done. Qed. -Check "notypeclasses_apply_test". -Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}. -Proof. - (* Partially applied lemma with typeclass in one of the trailing [_]. *) - notypeclasses apply (@decide (n = 0)). Show. -Restart. Proof. - (* Partially applied lemma with typeclass in one of the explicit [_]. *) - notypeclasses apply (@decide (n = 0) _). Show. -Abort. - Check "notypeclasses_apply_error". Lemma notypeclasses_apply_error (P Q : Prop) : (P → Q) → Q → P. Proof.