diff options
| author | Enrico Tassi | 2016-06-17 16:35:32 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-17 16:35:32 +0200 |
| commit | e33a23bbaefea57b486f7ea136ef4d058dbb34e1 (patch) | |
| tree | cd1fe48f75cffe4d94595926997803c3f57ecfe5 /mathcomp/ssrtest | |
| parent | 0e36c8f0247cbd814cd82592e2722b052283b495 (diff) | |
this test is now in Coq, removing it.
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. |