Imported Upstream version 8.5~beta1+dfsg

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3283.v b/test-suite/bugs/opened/3283.v
new file mode 100644
index 00000000..3ab5416e
--- /dev/null
+++ b/test-suite/bugs/opened/3283.v
@@ -0,0 +1,28 @@
+Notation "P |-- Q" := (@eq nat P Q) (at level 80, Q at level 41, no associativity) .
+Notation "x &&& y" := (plus x y) (at level 40, left associativity, y at next level) .
+Notation "'Ex' x , P " := (plus x P) (at level 65, x at level 99, P at level 80).
+
+(* Succeed *)
+Check _ |-- _ &&& _ -> _.
+Check _ |-- _ &&& (Ex _, _ ) -> _.
+Check _ |-- (_ &&& Ex _, _ ) -> _.
+
+(* Why does this fail? *)
+Fail Check _ |-- _ &&& Ex _, _  -> _.
+(* The command has indeed failed with message:
+=> Error: The term "Ex ?17, ?18" has type "nat"
+which should be Set, Prop or Type. *)
+
+(* Just in case something is strange with -> *)
+Notation "P ----> Q" := (P -> Q) (right associativity, at level 99, Q at next level).
+
+(* Succeed *)
+Check _ |-- _ &&& _ ----> _.
+Check _ |-- _ &&& (Ex _, _ )  ----> _.
+Check _ |-- (_ &&& Ex _, _ )  ----> _.
+
+(* Why does this fail? *)
+Fail Check _ |-- _ &&& Ex _, _  ----> _.
+(* The command has indeed failed with message:
+=> Error: The term "Ex ?31, ?32" has type "nat"
+which should be Set, Prop or Type.*)