From d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Apr 2014 16:44:02 +0200 Subject: Fix declarations of monomorphic assumptions --- test-suite/success/auto.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 9b691e253c..fb9f8c2182 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -14,7 +14,7 @@ Hint Resolve L. Goal G unit Q -> F (Q tt). intro. - auto. + eauto. Qed. (* Test implicit arguments in "using" clause *) -- cgit v1.2.3