diff options
author | 2014-12-11 15:48:31 +0100 | |
---|---|---|
committer | 2014-12-11 15:48:31 +0100 | |
commit | 2041981770992285798183754987eab25bf95181 (patch) | |
tree | 1063f763202ce3c99e8c5ccb89563f41a45e9ac0 /test-suite/bugs | |
parent | c938cb8e85f741ce697e7486d35c27c1aa31fe7a (diff) |
New reproduction cases for the test suite.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/opened/3819.v | 11 | ||||
-rw-r--r-- | test-suite/bugs/opened/3828.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/opened/3849.v | 8 |
3 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v new file mode 100644 index 000000000..7105a6587 --- /dev/null +++ b/test-suite/bugs/opened/3819.v @@ -0,0 +1,11 @@ +Set Universe Polymorphism. + +Record Op := { t : Type ; op : t -> t }. + +Canonical Structure OpType : Op := Build_Op Type (fun X => X). + +Lemma test1 (X:Type) : eq (op OpType X) X. +Proof eq_refl. + +Lemma test2 (A:Type) : eq (op _ A) A. +Fail Proof eq_refl. diff --git a/test-suite/bugs/opened/3828.v b/test-suite/bugs/opened/3828.v new file mode 100644 index 000000000..3cf0860b9 --- /dev/null +++ b/test-suite/bugs/opened/3828.v @@ -0,0 +1,2 @@ +Goal 0 = 0. +pose ?Goal. diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/opened/3849.v new file mode 100644 index 000000000..5290054a0 --- /dev/null +++ b/test-suite/bugs/opened/3849.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" hyp_list(hs) := clear hs. + +Tactic Notation "bar" hyp_list(hs) := foo hs. + +Goal True. +do 5 pose proof 0 as ?n0. +foo n1 n2. +Fail bar n3 n4. |