diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_110.v')
| -rw-r--r-- | 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/opened/HoTT_coq_110.v index 5ec40dbcb..c9874f898 100644 --- a/test-suite/bugs/opened/HoTT_coq_110.v +++ b/test-suite/bugs/opened/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. *) - Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) -End Y. + Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) +Fail End Y. |