diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 00:39:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 01:13:33 +0200 |
| commit | cd10b70637dea3cbba5785d163bc567a32a031a8 (patch) | |
| tree | 046d26c33c0b9a0a58bdf6d0d56c5e5dcaf919cd /test-suite/bugs/closed/3520.v | |
| parent | 593dfd66a5016ba457b6dccf1179a0e1ec7bff84 (diff) | |
Add test suite files for closed bugs.
Diffstat (limited to 'test-suite/bugs/closed/3520.v')
| -rw-r--r-- | test-suite/bugs/closed/3520.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v new file mode 100644 index 000000000..c981207e6 --- /dev/null +++ b/test-suite/bugs/closed/3520.v @@ -0,0 +1,12 @@ +Set Primitive Projections. + +Record foo (A : Type) := + { bar : Type ; baz := Set; bad : baz = bar }. + +Set Record Elimination Schemes. + +Record notprim : Prop := + { irrel : True; relevant : nat }. + + + |