New parsing/printing pattern/terms imp/scopes tests summarizing last changes.

2 files changed, 114 insertions, 0 deletions

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 9b50b53456..f59306c454 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -254,3 +254,59 @@ where
      : 0 = 0 /\ true = true
 ## 0 0 true
      : 0 = 0 /\ true = true
+# 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | # 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+#' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | #' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+## 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ## 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+##' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ##' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | P 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | P' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 49378ab846..09d5e31c48 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -338,3 +338,61 @@ Module AppliedTermsPrinting.
   End AtNotationForPartialApplication.
 
 End AppliedTermsPrinting.
+
+Module AppliedPatternsPrinting.
+
+  (* Other tests testing inheritance of scope and implicit in
+     term and pattern for parsing and printing *)
+
+  Inductive T := p (a:nat) (b:bool) {B} (b:B) : T.
+  Notation "0" := true : bool_scope.
+
+  Module A.
+  Notation "#" := @p (at level 0).
+  Check # 0 0 _ true.
+  Check fun a => match a with # 0 0 _ _ => 1 | _ => 2 end. (* !! *)
+  End A.
+
+  Module B.
+  Notation "#'" := p (at level 0).
+  Check #' 0 0 true.
+  Check fun a => match a with #' 0 0 _ => 1 | _ => 2 end.
+  End B.
+
+  Module C.
+  Notation "## q" := (@p q) (at level 0, q at level 0).
+  Check ## 0 0 true.
+  Check fun a => match a with ## 0 0 _ => 1 | _ => 2 end.
+  End C.
+
+  Module D.
+  Notation "##' q" := (p q) (at level 0, q at level 0).
+  Check ##' 0 0 true.
+  Check fun a => match a with ##' 0 0 _ => 1 | _ => 2 end.
+  End D.
+
+  Module E.
+  Notation P := @ p.
+  Check P 0 0 _ true.
+  Check fun a => match a with P 0 0 _ _ => 1 | _ => 2 end.
+  End E.
+
+  Module F.
+  Notation P' := p.
+  Check P' 0 0 true.
+  Check fun a => match a with P' 0 0 _ => 1 | _ => 2 end.
+  End F.
+
+  Module G.
+  Notation Q q := (@p q).
+  Check Q 0 0 true.
+  Check fun a => match a with Q 0 0 _ => 1 | _ => 2 end.
+  End G.
+
+  Module H.
+  Notation Q' q := (p q).
+  Check Q' 0 0 true.
+  Check fun a => match a with Q' 0 0 _ => 1 | _ => 2 end.
+  End H.
+
+End AppliedPatternsPrinting.