diff options
| author | Jasper Hugunin | 2019-01-19 18:20:36 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2019-02-22 10:28:45 -0800 |
| commit | c5e2f573ef079800eed4c8246c4f2bd39bf47b26 (patch) | |
| tree | c581b1ab6052bea7921b258070292140967b4ab6 /test-suite/success | |
| parent | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (diff) | |
Apply implicit binders to Hypothesis inside sections.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/AdvancedTypeClasses.v | 2 |
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. |