diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_110.v (renamed from test-suite/bugs/opened/HoTT_coq_110.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v index c9874f898c..5ec40dbcb9 100644 --- a/test-suite/bugs/opened/HoTT_coq_110.v +++ b/test-suite/bugs/closed/HoTT_coq_110.v @@ -19,5 +19,5 @@ Module Y. Definition foo : (A = B) * (A = B). split; abstract (rewrite <- P; reflexivity). (* Error: internal_paths_rew already exists. *) - Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) -Fail End Y. + Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) +End Y. |