diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 12:20:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 12:20:10 +0200 |
| commit | 5e1713d8fe9032a3f5c783cce288b409b6fdf816 (patch) | |
| tree | 7d9eacb8932c4cd3a7958100f3376612c4b7f8ae /test-suite/bugs/closed/3482.v | |
| parent | 707edf9b1e7310bd213678452950aaaa9e4e95f8 (diff) | |
Fix test-suite file after moving back to using C as the name
of the record binder for Class C's projections.
Diffstat (limited to 'test-suite/bugs/closed/3482.v')
| -rw-r--r-- | test-suite/bugs/closed/3482.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v index cf3f9dbef..34a5e73da 100644 --- a/test-suite/bugs/closed/3482.v +++ b/test-suite/bugs/closed/3482.v @@ -1,6 +1,6 @@ Set Primitive Projections. Class Foo (F : False) := { foo : True }. -Arguments foo F {f}. +Arguments foo F {Foo}. Print Implicit foo. (* foo : forall F : False, Foo F -> True Argument Foo is implicit and maximally inserted *) |