diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-05 10:49:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-05 10:49:29 -0400 |
| commit | 96d0f7f29cf15a6777353fa9b5a8b141aa06447d (patch) | |
| tree | ce9522d4435125a93410a08cb7f30b3e43b102ea /src/Util/Tactics | |
| parent | 2a94c03e5326020d63dd5a1afd4ab514ffb30a81 (diff) | |
Fix transparent assert by to respect names
Diffstat (limited to 'src/Util/Tactics')
| -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. |