From 75a8d43d1fec7ac4dd4325567a8252e3dc5b260c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jun 2014 14:15:25 +0200
Subject: Fix bug # 3325 using canonical structure declarations where needed.

---
 test-suite/bugs/closed/3325.v | 48 +++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3325.v | 50 -------------------------------------------
 2 files changed, 48 insertions(+), 50 deletions(-)
 create mode 100644 test-suite/bugs/closed/3325.v
 delete mode 100644 test-suite/bugs/opened/3325.v

diff --git a/test-suite/bugs/closed/3325.v b/test-suite/bugs/closed/3325.v
new file mode 100644
index 0000000000..36c065ebe8
--- /dev/null
+++ b/test-suite/bugs/closed/3325.v
@@ -0,0 +1,48 @@
+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". *)
diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v
deleted file mode 100644
index b84b1fb183..0000000000
--- a/test-suite/bugs/opened/3325.v
+++ /dev/null
@@ -1,50 +0,0 @@
-Unset Typeclass Resolution For Conversion.
-
-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". *)
-- 
cgit v1.2.3