aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_9329.v12
-rw-r--r--test-suite/unit-tests/lib/pp_big_vect.ml14
2 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v
new file mode 100644
index 0000000000..c0322dec40
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9329.v
@@ -0,0 +1,12 @@
+(* Declare empty levels in the same order they are computed *)
+
+Notation "< a ; b ; c >1" :=
+ (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
+Notation "< a ; b ; c >2" :=
+ (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
+Notation "< a ; b ; c >3" :=
+ (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
+Notation "< a ; b ; c >4" :=
+ (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
+Notation "< a ; b >" :=
+ (sum a b) (at level 61, a at level 63, b at level 62).
diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml
new file mode 100644
index 0000000000..e1cdd290e2
--- /dev/null
+++ b/test-suite/unit-tests/lib/pp_big_vect.ml
@@ -0,0 +1,14 @@
+open OUnit
+open Pp
+
+let pr_big_vect =
+ let n = "pr_big_vect" in
+ n >:: (fun () ->
+ let v = Array.make (1 lsl 20) () in
+ let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in
+ let str = string_of_ppcmds pp in
+ ignore(str))
+
+let tests = [pr_big_vect]
+
+let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests