diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-23 19:06:03 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-23 19:06:31 +0200 |
commit | efa3add0c03b70ecda3890cc6c69e66850605e7d (patch) | |
tree | 170f4a2991b8bfd30f6a769a173b2f0fe132686b /test-suite/bugs | |
parent | 550a407928063c8e93af808408a61a238fa5039a (diff) |
Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)
Every time you use abstract a kitten dies, please stop.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/3344.v (renamed from test-suite/bugs/opened/3344.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_111.v (renamed from test-suite/bugs/opened/HoTT_coq_111.v) | 13 |
2 files changed, 5 insertions, 8 deletions
diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/closed/3344.v index 8255fd6cc..8255fd6cc 100644 --- a/test-suite/bugs/opened/3344.v +++ b/test-suite/bugs/closed/3344.v diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/closed/HoTT_coq_111.v index deb8e6123..3b43f31df 100644 --- a/test-suite/bugs/opened/HoTT_coq_111.v +++ b/test-suite/bugs/closed/HoTT_coq_111.v @@ -1,5 +1,6 @@ + Module X. - Set Universe Polymorphism. + (*Set Universe Polymorphism.*) Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. @@ -7,13 +8,11 @@ Module X. Axiom P : A = B. Definition foo : A = B. abstract (rewrite <- P; reflexivity). - (* Error: internal_paths_rew already exists. *) - Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) - Admitted. + Defined. End X. Module Y. - Set Universe Polymorphism. + (*Set Universe Polymorphism.*) Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. @@ -21,7 +20,5 @@ Module Y. Axiom P : A = B. Definition foo : (A = B) * (A = B). split; abstract (rewrite <- P; reflexivity). - (* Error: internal_paths_rew already exists. *) - Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) - Admitted. + Defined. End Y. |