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

3 files changed, 49 insertions, 29 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0cbff51fb5..8a29fc3581 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -765,10 +765,10 @@ let extern_applied_ref inctx impl (cf,f) us args =
     let isproj = if !print_projections then isproj else None in
     CAppExpl ((isproj,f,us), args)
 
-let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
+let extern_applied_syntactic_definition inctx n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
-    let extraargs = adjust_implicit_arguments false n extraargs extraimpl in
+    let extraargs = adjust_implicit_arguments inctx n extraargs extraimpl in
     let args = syndefargs @ extraargs in
     if args = [] then cf else CApp ((None, CAst.make cf), args)
   with Expl ->
@@ -784,12 +784,12 @@ let mkFlattenedCApp (head,args) =
   | _ ->
     CApp ((None, head), args)
 
-let extern_applied_notation n impl f args =
+let extern_applied_notation inctx n impl f args =
   if List.is_empty args then
     f.CAst.v
   else
   try
-    let args = adjust_implicit_arguments false n args impl in
+    let args = adjust_implicit_arguments inctx n args impl in
     mkFlattenedCApp (f,args)
   with Expl -> raise No_match
 
@@ -940,11 +940,11 @@ let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 let rec extern inctx ?impargs scopes vars r =
   match remove_one_coercion inctx (flatten_application r) with
   | Some (nargs,inctx,r') ->
-    (try extern_notations scopes vars (Some nargs) r
+    (try extern_notations inctx scopes vars (Some nargs) r
      with No_match -> extern inctx scopes vars r')
   | None ->
 
-  try extern_notations scopes vars None r
+  try extern_notations inctx scopes vars None r
   with No_match ->
 
   let loc = r.CAst.loc in
@@ -1197,7 +1197,7 @@ and extern_local_binder scopes vars = function
         extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
       (assums,na::ids,
        CLocalDef(CAst.make na, extern false scopes vars bd,
-                   Option.map (extern false scopes vars) ty) :: l)
+                   Option.map (extern_typ scopes vars) ty) :: l)
 
     | GLocalAssum (na,bk,ty) ->
       let implicit_type = is_reserved_type na ty in
@@ -1225,14 +1225,14 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
-and extern_notations scopes vars nargs t =
+and extern_notations inctx scopes vars nargs t =
   if !Flags.raw_print || !print_no_symbol then raise No_match;
   try extern_possible_prim_token scopes t
   with No_match ->
   let t = flatten_application t in
-  extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+  extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
 
-and extern_notation (custom,scopes as allscopes) vars t rules =
+and extern_notation inctx (custom,scopes as allscopes) vars t rules =
   match rules with
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
@@ -1313,7 +1313,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                   let c = insert_entry_coercion coercion (insert_delimiters c key) in
                   let args = fill_arg_scopes args argsscopes allscopes in
                   let args = extern_args (extern true) vars args in
-                  CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
+                  CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args)
           | SynDefRule kn ->
               let l =
                 List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -1323,13 +1323,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               let a = CRef (cf,None) in
               let args = fill_arg_scopes args argsscopes allscopes in
               let args = extern_args (extern true) vars args in
-              let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
+              let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in
               if isCRef_no_univ c.CAst.v && entry_has_global custom then c
              else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
              | None -> raise No_match
              | Some coercion -> insert_entry_coercion coercion c
       with
-          No_match -> extern_notation allscopes vars t rules
+          No_match -> extern_notation inctx allscopes vars t rules
 
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c
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.