diff options
| author | Vincent Laporte | 2018-10-02 13:44:46 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-04 08:01:34 +0000 |
| commit | db22ae6140259dd065fdd80af4cb3c3bab41c184 (patch) | |
| tree | e17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/3325.v | |
| parent | 53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff) | |
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/closed/3325.v')
| -rw-r--r-- | test-suite/bugs/closed/3325.v | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/test-suite/bugs/closed/3325.v b/test-suite/bugs/closed/3325.v deleted file mode 100644 index 36c065ebe8..0000000000 --- a/test-suite/bugs/closed/3325.v +++ /dev/null @@ -1,48 +0,0 @@ -Typeclasses eauto := debug. -Set Printing All. - -Axiom SProp : Set. -Axiom sp : SProp. - -(* If we hardcode valueType := nat, it goes through *) -Class StateIs := { - valueType : Type; - stateIs : valueType -> SProp -}. - -Instance NatStateIs : StateIs := { - valueType := nat; - stateIs := fun _ => sp -}. -Canonical Structure NatStateIs. - -Class LogicOps F := { land: F -> F }. -Instance : LogicOps SProp. Admitted. -Instance : LogicOps Prop. Admitted. - -Parameter (n : nat). -(* If this is a [Definition], the resolution goes through fine. *) -Notation vn := (@stateIs _ n). -Definition vn' := (@stateIs _ n). -Definition GOOD : SProp := - @land _ _ vn'. -(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *) -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 |}. -Canonical Structure bi. - -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). -Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *) |
