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

Reviewed-by: SkySkimmer
Ack-by: herbelin

1 files changed, 22 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3667757a2f..43fef8685d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -636,10 +636,10 @@ exception Expl
 (* If the removal of implicit arguments is not possible, raise [Expl] *)
 (* [inctx] tells if the term is in a context which will enforce the external type *)
 (* [n] is the total number of arguments block to which the [args] belong *)
-let adjust_implicit_arguments inctx n q args impl =
-  let rec exprec q = function
+let adjust_implicit_arguments inctx n args impl =
+  let rec exprec = function
     | a::args, imp::impl when is_status_implicit imp ->
-        let tail = exprec (q+1) (args,impl) in
+        let tail = exprec (args,impl) in
         let visible =
           !Flags.raw_print ||
           (!print_implicits && !print_implicits_explicit_args) ||
@@ -652,13 +652,13 @@ let adjust_implicit_arguments inctx n q args impl =
           (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
         else
           tail
-    | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
+    | a::args, _::impl -> (Lazy.force a,None) :: exprec (args,impl)
     | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
     | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
       (* The non-explicit application cannot be parsed back with the same type *)
       raise Expl
     | [], _ -> []
-  in exprec q (args,impl)
+  in exprec (args,impl)
 
 let extern_projection (cf,f) args impl =
   let ip = is_projection (List.length args) cf in
@@ -750,14 +750,14 @@ let extern_applied_ref inctx impl (cf,f) us args =
     match extern_projection (cf,f) args impl with
     (* Try a [t.(f args1) args2] projection-style notation *)
     | Some (i,(args1,impl1),(args2,impl2)) ->
-      let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in
-      let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in
+      let args1 = adjust_implicit_arguments inctx n args1 impl1 in
+      let args2 = adjust_implicit_arguments inctx n args2 impl2 in
       let ip = Some (List.length args1) in
       CApp ((ip,f),args1@args2)
       (* A normal application node with each individual implicit
          arguments either dropped or made explicit *)
     | None ->
-      let args = adjust_implicit_arguments inctx n 1 args impl in
+      let args = adjust_implicit_arguments inctx n args impl in
       if args = [] then ref else CApp ((None, f), args)
   with Expl ->
   (* A [@f args] node *)
@@ -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 (n-List.length extraargs+1) 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 (n-List.length args+1) 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
@@ -1000,7 +1000,7 @@ let rec extern inctx ?impargs scopes vars r =
              mkFlattenedCApp (head,args))
 
   | GLetIn (na,b,t,c) ->
-      CLetIn (make ?loc na,sub_extern false scopes vars b,
+      CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
               Option.map (extern_typ scopes vars) t,
               extern inctx ?impargs scopes (add_vname vars na) c)
 
@@ -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