From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/opened/3283.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 test-suite/bugs/opened/3283.v (limited to 'test-suite/bugs/opened/3283.v') 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.*) -- cgit v1.2.3