diff options
Diffstat (limited to 'test-suite/bugs/opened/3377.v')
| -rw-r--r-- | test-suite/bugs/opened/3377.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/opened/3377.v deleted file mode 100644 index 23c0a965c..000000000 --- a/test-suite/bugs/opened/3377.v +++ /dev/null @@ -1,9 +0,0 @@ -Set Primitive Projections. -Set Implicit Arguments. -Record prod A B := pair { fst : A; snd : B}. - -Goal fst (@pair Type Type Type Type). -Set Printing All. -Fail match goal with |- ?f _ => idtac end. -(* Toplevel input, characters 7-44: -Error: No matching clauses for match. *) |