diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 16:44:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:59 +0200 |
| commit | d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c (patch) | |
| tree | ccb55617688c45b934ef6638332a99861324f840 /test-suite/success/auto.v | |
| parent | 2844926420c4a8436ce04711148a717c296c7236 (diff) | |
Fix declarations of monomorphic assumptions
Diffstat (limited to 'test-suite/success/auto.v')
| -rw-r--r-- | test-suite/success/auto.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 9b691e253..fb9f8c218 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 *) |