Add an option to disable typeclass resolution during conversion, which

is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.

1 files changed, 6 insertions, 2 deletions

diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v
index b4d1a79c0a..b84b1fb183 100644
--- a/test-suite/bugs/opened/3325.v
+++ b/test-suite/bugs/opened/3325.v
@@ -1,3 +1,5 @@
+Unset Typeclass Resolution For Conversion.
+
 Typeclasses eauto := debug.
 Set Printing All.
 
@@ -14,6 +16,7 @@ Instance NatStateIs : StateIs := {
   valueType := nat;
   stateIs := fun _ => sp
 }.
+Canonical Structure NatStateIs.
 
 Class LogicOps F := { land: F -> F }.
 Instance : LogicOps SProp. Admitted.
@@ -26,7 +29,7 @@ Definition vn' := (@stateIs _ n).
 Definition GOOD : SProp :=
   @land _ _ vn'.
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
-Fail Definition BAD : SProp :=
+Definition BAD : SProp :=
   @land _ _ vn.
 
 
@@ -36,6 +39,7 @@ 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).
@@ -43,4 +47,4 @@ 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". *)
+Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *)