diff options
| -rw-r--r-- | test-suite/bugs/closed/3828.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3828.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3828.v b/test-suite/bugs/closed/3828.v new file mode 100644 index 0000000000..ae11c6c96c --- /dev/null +++ b/test-suite/bugs/closed/3828.v @@ -0,0 +1,2 @@ +Goal 0 = 0. +Fail pose ?Goal. diff --git a/test-suite/bugs/opened/3828.v b/test-suite/bugs/opened/3828.v deleted file mode 100644 index 3cf0860b9b..0000000000 --- a/test-suite/bugs/opened/3828.v +++ /dev/null @@ -1,2 +0,0 @@ -Goal 0 = 0. -pose ?Goal. |