diff options
| author | Matthieu Sozeau | 2014-06-26 12:24:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-26 12:24:56 +0200 |
| commit | 24124a0f2708a798c3217991b8bd838622d78541 (patch) | |
| tree | 2dc6c721cbdafdc5f26f54a1396db33bcecf3fd1 | |
| parent | a8042c49ec2d49feb0d08630f758c6690297fbe6 (diff) | |
3392 is now closed thanks to E. Tassi.
| -rw-r--r-- | test-suite/bugs/closed/3392.v (renamed from test-suite/bugs/opened/3392.v) | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/3392.v b/test-suite/bugs/closed/3392.v index b28943e074..43acb7bb48 100644 --- a/test-suite/bugs/opened/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -37,5 +37,4 @@ Proof. rewrite eissect; apply apD ). -Fail Defined. -(* Anomaly: Uncaught exception Not_found(_). Please report. *) +Defined. |