[test-suite] test for primitive tokens in patterns

3 files changed, 45 insertions, 7 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 60213cab0c..cc9e745f6b 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -6,7 +6,7 @@
      : nat * nat * (nat * nat)
 (0, 2, (2, 2))
      : nat * nat * (nat * nat)
-pair (pair O (S (S O))) (pair (S (S O)) O)
+pair (pair 0 2) (pair 2 0)
      : prod (prod nat nat) (prod nat nat)
 << 0, 2, 4 >>
      : nat * nat * nat * (nat * (nat * nat))
@@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O)
      : nat * nat * nat * (nat * (nat * nat))
 (0, 2, 4, (0, (2, 4)))
      : nat * nat * nat * (nat * (nat * nat))
-pair (pair (pair O (S (S O))) (S (S (S (S O)))))
-  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+pair (pair (pair 0 2) 4) (pair 4 (pair 2 0))
      : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
 ETA x y : nat, Nat.add
      : nat -> nat -> nat
@@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t
      : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) *
        (nat * nat * nat)
 pair
-  (pair
-     (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O)))
-     (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O)))
+  (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0)))
+  (pair (pair 0 1) 2)
      : prod
          (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out
index cbed08c0ca..afe9b25442 100644
--- a/test-suite/output/primitive_tokens.out
+++ b/test-suite/output/primitive_tokens.out
@@ -2,6 +2,20 @@
      : string
 1234
      : nat
+Nat.add 1 2
+     : nat
+match "a" with
+| "a" => true
+| _ => false
+end
+     : bool
+match 1 with
+| 1 => true
+| _ => false
+end
+     : bool
+{| field := 7 |}
+     : test
 String (Ascii.Ascii false true true false false true true false)
   (String (Ascii.Ascii true true true true false true true false)
      (String (Ascii.Ascii true true true true false true true false)
@@ -27,3 +41,21 @@ S
                                                  (S
                                                  (S (S (S (S (S (S ...)))))))))))))))))))))))
      : nat
+Nat.add (S O) (S (S O))
+     : nat
+match
+  String (Ascii.Ascii true false false false false true true false)
+    EmptyString
+with
+| String (Ascii.Ascii true false false false false true true false)
+  EmptyString => true
+| _ => false
+end
+     : bool
+match S O with
+| S O => true
+| _ => false
+end
+     : bool
+{| field := S (S (S (S (S (S (S O)))))) |}
+     : test
diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v
index fe31107744..3207e5983f 100644
--- a/test-suite/output/primitive_tokens.v
+++ b/test-suite/output/primitive_tokens.v
@@ -1,5 +1,7 @@
 Require Import String.
 
+Record test := { field : nat }.
+
 Open Scope string_scope.
 
 Unset Printing Notations.
@@ -7,9 +9,15 @@ Unset Printing Notations.
 Check "foo".
 Check 1234.
 Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
 
-Unset Printing Primitive Tokens.
+Set Printing Raw Literals.
 
 Check "foo".
 Check 1234.
 Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.