aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/AdvancedTypeClasses.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/AdvancedTypeClasses.v')
-rw-r--r--test-suite/success/AdvancedTypeClasses.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index d0aa5c8578..0253ec46e4 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -71,7 +71,7 @@ Variable Inhabited: term -> Prop.
Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p.
Lemma L : Prop * A -> bool * (Type -> Set) .
-apply (Inhabited_correct _ _).
+apply Inhabited_correct.
change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
Admitted.