Merge PR #12877: Propagate in-context information for explicitation of extra arguments of notations

Reviewed-by: SkySkimmer
Ack-by: herbelin

4 files changed, 50 insertions, 16 deletions

diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 2265028d3e..d8b88b8c1c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -17,3 +17,7 @@ fix f (x : nat) : option nat := match x with
                                 | S _ => x
                                 end
      : nat -> option nat
+fun x : False => let y := False_rect (A:=bool) x in y
+     : False -> bool
+fun x : False => let y : True := False_rect x in y
+     : False -> True
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index a7c4399e38..86420bd8c8 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -61,3 +61,13 @@ Coercion some_nat := @Some nat.
 Check fix f x := match x with 0 => None | n => some_nat n end.
 
 End MatchBranchesInContext.
+
+Module LetInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+Axiom False_rect : forall A:Type, False -> A.
+Check fun x:False => let y:= False_rect (A:=bool) x in y. (* will not be in context: explicitation *)
+Check fun x:False => let y:= False_rect (A:=True) x in y. (* will be in context: no explicitation *)
+
+End LetInContext.
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.