diff options
| -rw-r--r-- | mathcomp/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssrtest/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssrtest/tacnotationpattern.v | 14 |
3 files changed, 0 insertions, 16 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index 9735a62..ef657d5 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -171,7 +171,6 @@ ssrtest/view_case.v ssrtest/wlogletin.v ssrtest/wlog_suff.v ssrtest/wlong_intro.v -ssrtest/tacnotationpattern.v ssreflect.ml4 -I . 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. |