From 96d0f7f29cf15a6777353fa9b5a8b141aa06447d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Apr 2017 10:49:29 -0400 Subject: Fix transparent assert by to respect names --- src/Util/Tactics/TransparentAssert.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/Tactics') diff --git a/src/Util/Tactics/TransparentAssert.v b/src/Util/Tactics/TransparentAssert.v index 533d159f7..576aab0e0 100644 --- a/src/Util/Tactics/TransparentAssert.v +++ b/src/Util/Tactics/TransparentAssert.v @@ -3,6 +3,6 @@ Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" := simple refine (let name := (_ : type) in _). (** [transparent eassert] is like [transparent assert], but allows holes in the type, which will be turned into evars. *) -Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" "by" tactic3(tac) := let name := fresh "H" in transparent assert (name : type); [ solve [ tac ] | ]. +Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" "by" tactic3(tac) := transparent assert (name : type); [ solve [ tac ] | ]. Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" := transparent assert (name : type). Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" "by" tactic3(tac) := transparent assert (name : type) by tac. -- cgit v1.2.3