diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 14:04:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 14:04:20 +0200 |
| commit | 4cd36df8879ae02639b3c8cf3712df6296e68a4c (patch) | |
| tree | caac3f1ae2aa12dad60120e50ac0b7d8cca354da /test-suite/bugs/opened/3325.v | |
| parent | 6281430231c9d4ea1353372678f1eb483e32a015 (diff) | |
| parent | 68bdb34f9e113233e1c0fe772a58d2393c8d6690 (diff) | |
Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonGross-tc
Diffstat (limited to 'test-suite/bugs/opened/3325.v')
| -rw-r--r-- | test-suite/bugs/opened/3325.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v index 4c221dc7f..b4d1a79c0 100644 --- a/test-suite/bugs/opened/3325.v +++ b/test-suite/bugs/opened/3325.v @@ -1,3 +1,6 @@ +Typeclasses eauto := debug. +Set Printing All. + Axiom SProp : Set. Axiom sp : SProp. @@ -16,7 +19,6 @@ Class LogicOps F := { land: F -> F }. Instance : LogicOps SProp. Admitted. Instance : LogicOps Prop. Admitted. -Set Printing All. Parameter (n : nat). (* If this is a [Definition], the resolution goes through fine. *) Notation vn := (@stateIs _ n). @@ -26,3 +28,19 @@ Definition GOOD : SProp := (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *) Fail Definition BAD : SProp := @land _ _ vn. + + +Class A T := { foo : T -> Prop }. +Instance: A nat. Admitted. +Instance: A Set. Admitted. + +Class B := { U : Type ; b : U }. +Instance bi: B := {| U := nat ; b := 0 |}. + +Notation b0N := (@b _ : nat). +Notation b0Ni := (@b bi : nat). +Definition b0D := (@b _ : nat). +Definition GOOD1 := (@foo _ _ b0D). +Definition GOOD2 := (let x := b0N in @foo _ _ x). +Definition GOOD3 := (@foo _ _ b0Ni). +Fail Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *) |