diff options
| author | Matthieu Sozeau | 2014-06-20 16:06:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-20 16:06:06 +0200 |
| commit | a57c7612767f7bd55704639f03c0899d5c3edfbb (patch) | |
| tree | 19ce904a2b2515f1217a6dcf11abad5e12528687 | |
| parent | 6133a43c30e03656696a897bcedaf0cfb2cec70d (diff) | |
Fixed bug 3332.
| -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. *) |