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.

2 files changed, 24 insertions, 20 deletions

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.