diff options
| -rw-r--r-- | test-suite/bugs/opened/3332.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/test-suite/bugs/opened/3332.v b/test-suite/bugs/opened/3332.v deleted file mode 100644 index 275eaea5d9..0000000000 --- a/test-suite/bugs/opened/3332.v +++ /dev/null @@ -1,6 +0,0 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-time") -*- *) -Definition foo : True. -Proof. -Abort. (* Toplevel input, characters 15-21: -Anomaly: Backtrack.backto to a state with no vcs_backup. Please report. *) -(* Anomaly: VernacAbort not handled by Stm. Please report. *) |