diff options
| -rw-r--r-- | test-suite/bugs/opened/3377.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/opened/3377.v index 9ad3779d16..23c0a965c8 100644 --- a/test-suite/bugs/opened/3377.v +++ b/test-suite/bugs/opened/3377.v @@ -1,4 +1,5 @@ Set Primitive Projections. +Set Implicit Arguments. Record prod A B := pair { fst : A; snd : B}. Goal fst (@pair Type Type Type Type). |