diff options
Diffstat (limited to 'test-suite/bugs/opened/3298.v')
-rw-r--r-- | test-suite/bugs/opened/3298.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v deleted file mode 100644 index bce7c3f2..00000000 --- a/test-suite/bugs/opened/3298.v +++ /dev/null @@ -1,23 +0,0 @@ -Module JGross. - Hint Extern 1 => match goal with |- match ?E with end => case E end. - - Goal forall H : False, match H return Set with end. - Proof. - intros. - Fail solve [ eauto ]. (* No applicable tactic *) - admit. - Qed. -End JGross. - -Section BenDelaware. - Hint Extern 0 => admit. - Goal forall (H : False), id (match H return Set with end). - Proof. - eauto. - Qed. - Goal forall (H : False), match H return Set with end. - Proof. - Fail solve [ eauto ] . - admit. - Qed. -End BenDelaware. |