aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3325.v
diff options
context:
space:
mode:
authorVincent Laporte2018-10-02 13:44:46 +0000
committerVincent Laporte2018-10-04 08:01:34 +0000
commitdb22ae6140259dd065fdd80af4cb3c3bab41c184 (patch)
treee17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/3325.v
parent53929e9bacf251f60c85d4ff24d46fec2c42ab4b (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.v48
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". *)