diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_110.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_110.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v new file mode 100644 index 00000000..5ec40dbc --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_110.v @@ -0,0 +1,23 @@ +Module X. + Inductive paths A (x : A) : A -> Type := idpath : paths A x x. + Notation "x = y" := (@paths _ x y) : type_scope. + + Axioms A B : Type. + Axiom P : A = B. + Definition foo : A = B. + abstract (rewrite <- P; reflexivity). + (* Error: internal_paths_rew already exists. *) + Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) +End X. + +Module Y. + Inductive paths A (x : A) : A -> Type := idpath : paths A x x. + Notation "x = y" := (@paths _ x y) : type_scope. + + Axioms A B : Type. + Axiom P : A = B. + 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. |