From c25f2b7d14aa522dd6e2ec7da7cbb9dddbc6688b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Oct 2018 12:13:10 +0100 Subject: [ssr] better doc for the IPatDispatch AST --- test-suite/bugs/closed/8544.v | 6 ------ test-suite/bugs/closed/bug_8544.v | 6 ++++++ 2 files changed, 6 insertions(+), 6 deletions(-) delete mode 100644 test-suite/bugs/closed/8544.v create mode 100644 test-suite/bugs/closed/bug_8544.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/8544.v b/test-suite/bugs/closed/8544.v deleted file mode 100644 index 674d112595..0000000000 --- a/test-suite/bugs/closed/8544.v +++ /dev/null @@ -1,6 +0,0 @@ -Require Import ssreflect. -Goal True \/ True -> False. -Proof. -(* the following should fail: 2 subgoals, but only one intro pattern *) -Fail case => [a]. -Abort. diff --git a/test-suite/bugs/closed/bug_8544.v b/test-suite/bugs/closed/bug_8544.v new file mode 100644 index 0000000000..674d112595 --- /dev/null +++ b/test-suite/bugs/closed/bug_8544.v @@ -0,0 +1,6 @@ +Require Import ssreflect. +Goal True \/ True -> False. +Proof. +(* the following should fail: 2 subgoals, but only one intro pattern *) +Fail case => [a]. +Abort. -- cgit v1.2.3