diff options
| -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. |