diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-18 16:43:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-18 16:43:40 +0200 |
| commit | c61e5783458d4b9f2cd104bd027893f6bdc82ded (patch) | |
| tree | f006a40a50d9c121a36e214e49512ae097b0ca35 | |
| parent | d40751a0270a60918ea6385edb53b1406ba990d5 (diff) | |
Fix test-suite file.
| -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 9ad3779d1..23c0a965c 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). |