diff options
Diffstat (limited to 'test-suite/bugs/opened/3849.v')
| -rw-r--r-- | test-suite/bugs/opened/3849.v | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/opened/3849.v deleted file mode 100644 index 5290054a..00000000 --- a/test-suite/bugs/opened/3849.v +++ /dev/null @@ -1,8 +0,0 @@ -Tactic Notation "foo" hyp_list(hs) := clear hs. - -Tactic Notation "bar" hyp_list(hs) := foo hs. - -Goal True. -do 5 pose proof 0 as ?n0. -foo n1 n2. -Fail bar n3 n4. |