diff options
Diffstat (limited to 'src/Util/Tactics/TransparentAssert.v')
| -rw-r--r-- | src/Util/Tactics/TransparentAssert.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |