From 62990950858ef2e40639d1bae79620db5ce4e37e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 11 Aug 2016 15:56:37 -0700 Subject: Don't take advantage of design flaws (auto with *) See bug #4966, https://coq.inria.fr/bugs/show_bug.cgi?id=4966. --- src/Util/Tactics.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Util/Tactics.v') 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 -- cgit v1.2.3