Propagate in-context information for extra arguments of notations too.

2 files changed, 36 insertions, 16 deletions

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index f59306c454..a6c2553a89 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -146,8 +146,10 @@ v
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 @v 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-v 0 (B:=bool)
+v 0
      : forall b : bool, 0 = 0 /\ b = b
+     = ?n@{x:=v 0 (B:=bool)}
+     : nat
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 v 0
@@ -166,8 +168,10 @@ v
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 @v 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-v 0 (B:=bool)
+v 0
      : forall b : bool, 0 = 0 /\ b = b
+     = ?n@{x:=v 0 (B:=bool)}
+     : nat
 ##
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
@@ -192,10 +196,12 @@ where
      : 0 = 0 /\ true = true
 ## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
+     = ?n@{x:=## 0 0 (B:=bool)}
+     : nat
 ## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
@@ -230,10 +236,12 @@ where
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
+     = ?n@{x:=## 0 0 (B:=bool)}
+     : nat
 ## 0 0 true
      : 0 = 0 /\ true = true
 ## 0 0 true
@@ -246,10 +254,12 @@ where
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool)
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
+     = ?n@{x:=## 0 0 (B:=bool)}
+     : nat
 ## 0 0 true
      : 0 = 0 /\ true = true
 ## 0 0 true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 09d5e31c48..010b0da4a9 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -189,7 +189,9 @@ Module AppliedTermsPrinting.
   Check @v 0.
   (* @v 0 *)
   Check @p nat 0 0 bool.
-  (* v 0 (B:=bool) *)
+  (* v 0 *)
+  Eval simpl in (fun x => _:nat) (@p nat 0 0 bool).
+  (* ?n@{x:=v 0 (B:=bool)} *)
 
   End AtAbbreviationForPartialApplication.
 
@@ -217,7 +219,9 @@ Module AppliedTermsPrinting.
   Check @v 0.
   (* @v 0 *)
   Check @p nat 0 0 bool.
-  (* v 0 (B:=bool) *)
+  (* v 0 *)
+  Eval simpl in (fun x => _:nat) (@p nat 0 0 bool).
+  (* ?n@{x:=v 0 (B:=bool)} *)
 
   End AbbreviationForPartialApplication.
 
@@ -247,9 +251,11 @@ Module AppliedTermsPrinting.
   Check ## 0 0 true.
   (* ## 0 0 true *)
   Check p 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
   Check ## 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
+  Eval simpl in (fun x => _:nat) (@p nat 0 0 bool).
+  (* ?n@{x:=## 0 0 (B:=bool)} *)
 
   End NotationForHeadApplication.
 
@@ -301,9 +307,11 @@ Module AppliedTermsPrinting.
   Check ## 0 0.
   (* ## 0 0 *)
   Check p 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
   Check ## 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
+  Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)).
+  (* ?n@{## 0 0 (B:=bool)} *)
   Check p 0 0 true.
   (* ## 0 0 true *)
   Check ## 0 0 true.
@@ -327,9 +335,11 @@ Module AppliedTermsPrinting.
   Check ## 0 0.
   (* ## 0 0 *)
   Check p 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
   Check ## 0 0 (B:=bool).
-  (* ## 0 0 (B:=bool) *)
+  (* ## 0 0 *)
+  Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)).
+  (* ?n@{## 0 0 (B:=bool)} *)
   Check p 0 0 true.
   (* ## 0 0 true *)
   Check ## 0 0 true.