diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_111.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_111.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v index 56feadb40..825a26e16 100644 --- a/test-suite/bugs/opened/HoTT_coq_111.v +++ b/test-suite/bugs/opened/HoTT_coq_111.v @@ -6,9 +6,10 @@ Module X. Axioms A B : Type. Axiom P : A = B. Definition foo : A = B. - abstract (rewrite <- P; reflexivity). + Fail abstract (rewrite <- P; reflexivity). (* Error: internal_paths_rew already exists. *) - Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) + Admitted. + Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) End X. Module Y. @@ -19,7 +20,7 @@ Module Y. Axioms A B : Type. Axiom P : A = B. Definition foo : (A = B) * (A = B). - split; abstract (rewrite <- P; reflexivity). + Fail 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. |