4 files changed, 26 insertions, 2 deletions
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 44d21b83..b8cae471 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -12,3 +12,20 @@ Record Silly (X : Set) : Set := mkSilly { x : X }.
 Definition anotherMk := mkSilly.
 Definition struct := anotherMk nat 3.
 Canonical Structure struct.
+
+(* Intertwinning canonical structures and delta-expansion *)
+(* Assia's short example *)
+
+Open Scope bool_scope.
+
+Set Implicit Arguments.
+
+Structure test_struct : Type := mk_test {dom :> Type; f : dom -> dom -> bool}.
+
+Notation " x != y":= (f _ x y)(at level 10).
+
+Canonical Structure bool_test := mk_test (fun x y => x || y).
+
+Definition b := bool.
+
+Check (fun x : b => x != x).
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index e7795733..84ec298d 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,6 +2,8 @@ Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
 
+Implicit Arguments vector [].
+
 Require Import Coq.Program.Program.
 
 Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n :=
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index facd5509..6dce0401 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -21,3 +21,8 @@ Definition marker := O.
 Notation "x +1" := (S x) (at level 8, left associativity).
 Reset marker.
 Notation "x +1" := (S x) (at level 8, right associativity).
+
+(* Check that empty levels (here 8 and 2 in pattern) are added in the
+   right order *)
+
+Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 34fff9d1..b89787bb 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
 Axiom SetoidS1 : Setoid_Theory S1 eqS1.
 Add Setoid S1 eqS1 SetoidS1 as S1setoid.
 
-Instance eqS1_default : DefaultRelation S1 eqS1.
+Instance eqS1_default : DefaultRelation eqS1.
 
 Axiom eqS1': S1 -> S1 -> Prop.
 Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
 Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
 Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
 
-Instance eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation eqS1_test8.
 
 Axiom f_test8 : S2 -> S1_test8.
 Add Morphism f_test8 : f_compat_test8. Admitted.