From d6467c2fea8a29634ca649850784c95ed5b9d4f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 13:17:12 +0100
Subject: Fixing anomaly from #11091 (incompatible printing with notation and
 imp. args).

We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
---
 test-suite/output/Notations5.out | 20 ++++++++++++--------
 test-suite/output/Notations5.v   | 24 ++++++++++++------------
 2 files changed, 24 insertions(+), 20 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index c5b4d6f291..96687ed07f 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -138,7 +138,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -158,7 +158,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -188,9 +188,9 @@ where
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
@@ -226,23 +226,27 @@ p 0 0 true
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index b3bea929ba..3c25547aac 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -181,7 +181,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -209,7 +209,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -243,9 +243,9 @@ Module AppliedTermsPrinting.
   Check ## 0 0.
   (* ## 0 0 *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 (B:=bool).
@@ -298,16 +298,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* @p nat 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 bool.
   (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
 
   End NotationForPartialApplication.
 
@@ -324,16 +324,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* @p nat 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 bool.
   (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true -- INCONSISTENCY parsing/printing *)
 
   End AtNotationForPartialApplication.
 
-- 
cgit v1.2.3


From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:19:27 +0100
Subject: Fixing a notation printing bug (missing a @ to reflect absence of
 imp. args).

When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
---
 test-suite/output/Notations5.out | 4 ++--
 test-suite/output/Notations5.v   | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 96687ed07f..7afb5ad396 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -104,9 +104,9 @@ u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 3c25547aac..92ac4b03ff 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -145,9 +145,9 @@ Module AppliedTermsPrinting.
   Check p.
   (* u *)
   Check @p.
-  (* u -- BUG *)
+  (* @u *)
   Check @u.
-  (* u -- BUG *)
+  (* @u *)
   Check u.
   (* u *)
   Check p 0 0.
-- 
cgit v1.2.3


From 67e16fdeef26455d0afa357e31de8f7b3f772034 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:30:05 +0100
Subject: Fixing printing of notations bound to an expression of the form "@f".

The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.

It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
---
 test-suite/output/Notations5.out | 30 +++++++++++++++---------------
 test-suite/output/Notations5.v   | 30 +++++++++++++++---------------
 2 files changed, 30 insertions(+), 30 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 7afb5ad396..9287ea1d4f 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,27 +78,27 @@ f
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
 f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-p
+u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-p
+u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0 0
+u 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+u 0 0
      : forall b : bool, 0 = 0 /\ b = b
-@p nat 0 0
+@u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@p nat 0 0
+@u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -196,7 +196,7 @@ where
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-p
+##
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,23 +204,23 @@ where
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 ##
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0
+## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0
+## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 @p nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-p 0 0
+## 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 92ac4b03ff..81cedc03b4 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* p *)
+  (* u -- INCONSISTENT parsing/printing *)
   Check p.
-  (* p *)
-  Check @p.
   (* u *)
+  Check @p.
+  (* @u -- INCONSISTENT parsing/printing *)
   Check u.
-  (* u *)
+  (* @u -- INCONSISTENT parsing/printing *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* u 0 0 *)
   Check u nat 0 0 bool.
-  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  (* u 0 0 -- INCONSISTENT parsing/printing *)
   Check u nat 0 0.
-  (* @p nat 0 0 *)
+  (* @u nat 0 0 *)
   Check @p nat 0 0.
-  (* @p nat 0 0 *)
+  (* @u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* p *)
+  (* ## -- INCONSISTENT parsing/printing *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* p 0 -- why not "## nat 0" *)
+  (* ## 0 *)
   Check ## nat 0.
-  (* p 0 *)
+  (* ## 0 -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0.
   (* @p nat 0 0 *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* ## 0 0 *)
   Check ## nat 0 0 _.
-  (* p 0 0 *)
+  (* ## 0 0 -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0 bool.
-  (* p 0 0 (B:=bool) *)
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0 bool true.
-  (* p 0 0 true *)
+  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
 
   End AtNotationForHeadApplication.
 
-- 
cgit v1.2.3


From 556e9dde62b6822db20bd5c7e6e6a67bc717c408 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:31:37 +0100
Subject: Deactivate implicit arguments in printing notations bound to "@f".

This is to match the parsing policy (see #11091).

In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
---
 test-suite/output/Notations.out  |  9 +++++----
 test-suite/output/Notations5.out | 32 ++++++++++++++++----------------
 test-suite/output/Notations5.v   | 32 ++++++++++++++++----------------
 3 files changed, 37 insertions(+), 36 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..2966c1126d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,10 +111,11 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T => match x with
-                   | NIL => NONE2
-                   | (_ :') t => SOME2 t
-                   end
+fun x : list ?T =>
+match x with
+| NIL => NONE3 (list ?T)
+| (_ :') t => SOME3 (list ?T) t
+end
      : list ?T -> option (list ?T)
 where
 ?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 9287ea1d4f..990a7151b4 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,27 +78,27 @@ f
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
 f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u 0 0
+u nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-u 0 0
+u nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-@u nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@u nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -196,7 +196,7 @@ where
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-##
+## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,23 +204,23 @@ where
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 ##
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
+## nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 true
+## nat 0 0 bool true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 81cedc03b4..0b78c388fa 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* u -- INCONSISTENT parsing/printing *)
+  (* u ?A *)
   Check p.
-  (* u *)
+  (* u ?A *)
   Check @p.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check u.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check p 0 0.
-  (* u 0 0 *)
+  (* u nat 0 0 ?B *)
   Check u nat 0 0 bool.
-  (* u 0 0 -- INCONSISTENT parsing/printing *)
+  (* u nat 0 0 bool *)
   Check u nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
   Check @p nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* ## -- INCONSISTENT parsing/printing *)
+  (* ## ?A *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* ## 0 *)
+  (* ## nat 0 *)
   Check ## nat 0.
-  (* ## 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 *)
   Check ## nat 0 0.
-  (* @p nat 0 0 *)
+  (* ## nat 0 0 *)
   Check p 0 0.
-  (* ## 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 _.
-  (* ## 0 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool *)
   Check ## nat 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool true *)
 
   End AtNotationForHeadApplication.
 
-- 
cgit v1.2.3


From 14196d8ab425f67faf3995bd29a003de3b2e87ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:26:14 +0100
Subject: Propagate implicit arguments in all notations for partial
 applications.

This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
---
 test-suite/output/Notations5.out | 12 ++++++++----
 test-suite/output/Notations5.v   | 20 ++++++++++----------
 test-suite/success/Notations2.v  | 26 +++++++++++++-------------
 3 files changed, 31 insertions(+), 27 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 990a7151b4..9b50b53456 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -226,8 +226,10 @@ where
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
-     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
@@ -240,8 +242,10 @@ where
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
-     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 0b78c388fa..49378ab846 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -299,15 +299,15 @@ Module AppliedTermsPrinting.
   Check ## 0.
   (* ## 0 *)
   Check ## 0 0.
-  (* @p nat 0 0 *)
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
   (* ## 0 0 true *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End NotationForPartialApplication.
 
@@ -325,15 +325,15 @@ Module AppliedTermsPrinting.
   Check ## 0.
   (* ## 0 *)
   Check ## 0 0.
-  (* @p nat 0 0 *)
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
   (* ## 0 0 true *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENCY parsing/printing *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End AtNotationForPartialApplication.
 
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index b26e725d9b..986908b7fc 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -7,21 +7,21 @@ The convention is:
 Constant foo with implicit arguments and scopes used in a term or a pattern:
 
        foo      do not deactivate further arguments and scopes
-       @foo     deactivates further arguments and scopes
-       (foo x)  deactivates further arguments and scopes
-       (@foo x) deactivates further arguments and scopes
+       @foo     deactivate further arguments and scopes
+       (foo x)  deactivate further arguments and scopes
+       (@foo x) deactivate further arguments and scopes
 
 Notations binding to foo:
 
 #   := foo      do not deactivate further arguments and scopes
-#   := @foo     deactivates further arguments and scopes
-# x := foo x    deactivates further arguments and scopes
-# x := @foo x   deactivates further arguments and scopes
+#   := @foo     deactivate further arguments and scopes
+# x := foo x    do not deactivate further arguments and scopes
+# x := @foo x   do not deactivate further arguments and scopes
 
 Abbreviations binding to foo:
 
 f   := foo      do not deactivate further arguments and scopes
-f   := @foo     deactivates further arguments and scopes
+f   := @foo     deactivate further arguments and scopes
 f x := foo x    do not deactivate further arguments and scopes
 f x := @foo x   do not deactivate further arguments and scopes
 *)
@@ -62,17 +62,17 @@ Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 
-(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 5. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
-Check # 0 _ 0%bool 0%bool : prod' bool bool.
+Check # 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
 
-(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
-Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ## 0%bool 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
@@ -86,9 +86,9 @@ Notation "####" := pair' (at level 0).
 Check #### 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 
-(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+(* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
-Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
+Check ##### 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
-- 
cgit v1.2.3


From 04b9870f0ebe79fde789551c8e172aad1e7cfc5c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:52:01 +0100
Subject: Inherit argument scopes in notations to expressions of the form @f.

This is a change of semantics.
---
 test-suite/success/Notations2.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 986908b7fc..dca0208fb0 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -185,3 +185,12 @@ Import A.
 Infix "+++" := Nat.add (at level 80).
 
 End M18.
+
+Module InheritanceArgumentScopes.
+
+Axiom p : forall (A:Type) (b:nat), A = A /\ b = b.
+Check fun A n => p (A * A) (n * n). (* safety check *)
+Notation q := @p.
+Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *)
+
+End InheritanceArgumentScopes.
-- 
cgit v1.2.3


From ba52fd0dff4dcf06621fb91ff4902a060a0b222d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 11:36:51 +0100
Subject: Use auxiliary function for externing record patterns.

Also apply the same conditions for printing constructors as record
instances in both terms and patterns.
---
 test-suite/output/Record.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index d9a649fadc..71a8afa131 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,6 +20,8 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
+Set Printing Records.
+
 Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
-- 
cgit v1.2.3


From 8d80875d230bd8af5611ec04bced1e5a17d058b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:46:42 +0100
Subject: Inherit scopes and implicit sign. in notations for partially applied
 pattern.

Exception: when the notation is to some @id.

Formerly, this was ignored for all kinds of string notations.
---
 test-suite/success/Notations2.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index dca0208fb0..f166a53256 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -66,14 +66,14 @@ Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2
 Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
 Check # 0 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end.
 
 (* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
 Check ## 0%bool 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
 Notation "###" := (@pair') (at level 0).
@@ -89,7 +89,7 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 (* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
 Check ##### 0 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
 (* it should be detected as binding variable and the scopes not being checked *)
-- 
cgit v1.2.3


From 9da7715108554a5105c012685e90b2fa563abf08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:41:00 +0100
Subject: In printing patterns, distinguish the case of a notation to @id.

This is a case which conventionally deactivates implicit arguments.
---
 test-suite/output/Notations.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2966c1126d..53ad8a9612 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -107,8 +107,8 @@ fun x : option Z => match x with
                     end
      : option Z -> Z
 fun x : option Z => match x with
-                    | SOME2 x0 => x0
-                    | NONE2 => 0
+                    | SOME3 _ x0 => x0
+                    | NONE3 _ => 0
                     end
      : option Z -> Z
 fun x : list ?T =>
-- 
cgit v1.2.3


From 02cdbd221183b985460dedd49d74b07f4b647bcd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 14:24:32 +0100
Subject: New parsing/printing pattern/terms imp/scopes tests summarizing last
 changes.

---
 test-suite/output/Notations5.out | 56 ++++++++++++++++++++++++++++++++++++++
 test-suite/output/Notations5.v   | 58 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 114 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From bf1e15181a2531a106fa643ca8e9233cb889af12 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Nov 2019 21:49:47 +0100
Subject: Fixes #4690: do not allow @f in notations when f is a notation
 variable.

---
 test-suite/bugs/bug_4690.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/bug_4690.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v
new file mode 100644
index 0000000000..f50866a990
--- /dev/null
+++ b/test-suite/bugs/bug_4690.v
@@ -0,0 +1,3 @@
+(* Check that @f is not allowed in notation when f is a notation variable *)
+
+Fail Notation "# g" := (@g O) (at level 0).
-- 
cgit v1.2.3