diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-11 15:56:37 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-11 15:56:37 -0700 |
| commit | 62990950858ef2e40639d1bae79620db5ce4e37e (patch) | |
| tree | 26a4b3ec6ee68b66fb3a8862642e788046344cbb /src/Util/Tactics.v | |
| parent | 8c106350250c61b06afeb64d580212abd6c63ab2 (diff) | |
Don't take advantage of design flaws (auto with *)
See bug #4966, https://coq.inria.fr/bugs/show_bug.cgi?id=4966.
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 4559a1757..880f5824a 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -252,6 +252,12 @@ Ltac specialize_by' tac := Ltac specialize_by tac := repeat specialize_by' tac. +(** [specialize_by auto] should not mean [specialize_by ltac:( auto + with * )]!!!!!!! (see + https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design + flaw. *) +Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does |