From 580b25e05c7cc9e7a31430b3d9edb14ae12b7598 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 11 Sep 2014 20:47:06 +0200 Subject: Fix test-suite files, and move some opened to closed. --- test-suite/bugs/closed/3482.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/3482.v') diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v index 34a5e73da..cf3f9dbef 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 {Foo}. +Arguments foo F {f}. Print Implicit foo. (* foo : forall F : False, Foo F -> True Argument Foo is implicit and maximally inserted *) -- cgit v1.2.3