aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 14:41:36 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 14:41:36 +0200
commit9326b0466cc04175436dc57cf0283c151b587e54 (patch)
treeefa25b429b80403105431c8ea21bae475dffea8e /test-suite/bugs
parent57af4b4112dd0bc54badf0faebb373ef70ea2c1a (diff)
parent414a30432119bcc878793b33144f671403132f7a (diff)
Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructuration
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/5469.v3
-rw-r--r--test-suite/bugs/closed/5608.v33
2 files changed, 33 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
deleted file mode 100644
index fce671c75..000000000
--- a/test-suite/bugs/closed/5469.v
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Some problems with the special treatment of curly braces *)
-
-Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v
new file mode 100644
index 000000000..f02eae69c
--- /dev/null
+++ b/test-suite/bugs/closed/5608.v
@@ -0,0 +1,33 @@
+Reserved Notation "'slet' x .. y := A 'in' b"
+ (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b").
+Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
+ (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )").
+
+Delimit Scope ctype_scope with ctype.
+Local Open Scope ctype_scope.
+Delimit Scope expr_scope with expr.
+Inductive base_type := TZ | TWord (logsz : nat).
+Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type).
+Context {var : base_type -> Type}.
+Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t :
+flat_type) :=
+ match t with
+ | Tbase t => interp_base_type t
+ | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type
+interp_base_type y)
+ end.
+Inductive exprf : flat_type -> Type :=
+| Var {t} (v : var t) : exprf (Tbase t)
+| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) :
+exprf tC
+| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty).
+Global Arguments Var {_} _.
+Global Arguments LetIn {_} _ {_} _.
+Global Arguments Pair {_} _ {_} _.
+Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A
+(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope.
+Definition foo :=
+ (fun x3 =>
+ (LetIn (Var x3) (fun x18 : var TZ
+ => (Pair (Var x18) (Var x18))))).
+Print foo.