diff options
Diffstat (limited to 'mathcomp/ssrtest')
| -rw-r--r-- | mathcomp/ssrtest/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssrtest/tacnotationpattern.v | 14 |
2 files changed, 0 insertions, 15 deletions
diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make index 716dc4a..ab4c666 100644 --- a/mathcomp/ssrtest/Make +++ b/mathcomp/ssrtest/Make @@ -39,7 +39,6 @@ view_case.v wlogletin.v wlog_suff.v wlong_intro.v -tacnotationpattern.v -R ../theories Ssreflect -I ../src/ diff --git a/mathcomp/ssrtest/tacnotationpattern.v b/mathcomp/ssrtest/tacnotationpattern.v deleted file mode 100644 index 13de4bc..0000000 --- a/mathcomp/ssrtest/tacnotationpattern.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import mathcomp.ssreflect.ssreflect. -Tactic Notation "at" ssrpatternarg(p) tactic(t) - := - ssrpattern p; let top := fresh in intro top; - t top; try unfold top in * |- *; try clear top. - -Goal forall x y, x + y = 4. -intros. -at [RHS] (fun top => remember top as E eqn:E_def). -match goal with -| |- x + y = E => idtac -| |- _ => fail -end. -Admitted. |