From d6467c2fea8a29634ca649850784c95ed5b9d4f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 13:17:12 +0100
Subject: 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.
---
 interp/constrextern.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38dc10a9b3..82ba559406 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -742,7 +742,7 @@ let extern_applied_ref inctx impl (cf,f) us args =
 let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
-    let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in
+    let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in
     let args = syndefargs @ extraargs in
     if args = [] then cf else CApp ((None, CAst.make cf), args)
   with Expl ->
@@ -762,8 +762,10 @@ let extern_applied_notation n impl f args =
   if List.is_empty args then
     f.CAst.v
   else
-    let args = adjust_implicit_arguments false (List.length args) 1 args impl in
+  try
+    let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in
     mkFlattenedCApp (f,args)
+  with Expl -> raise No_match
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
-- 
cgit v1.2.3


From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:19:27 +0100
Subject: Fixing a notation printing bug (missing a @ to reflect absence of
 imp. args).

When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
---
 interp/constrextern.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82ba559406..5098b2a00c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1216,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
               (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
               args2, args2scopes, args2impls
-          | None when nallargs > 0 ->
+          | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
@@ -1226,7 +1226,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
             | _ -> t, [], [], []
             end
-          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
-- 
cgit v1.2.3


From 67e16fdeef26455d0afa357e31de8f7b3f772034 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:30:05 +0100
Subject: Fixing printing of notations bound to an expression of the form "@f".

The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.

It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
---
 interp/constrextern.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5098b2a00c..681d6ba541 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1209,23 +1209,17 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n && nallargs > 0 ->
+          | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
               (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
-              (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-              args2, args2scopes, args2impls
+              DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | Some 0 when nallargs = 0 ->
-            begin match DAst.get f with
-            | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
-            | _ -> t, [], [], []
-            end
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
-- 
cgit v1.2.3


From 556e9dde62b6822db20bd5c7e6e6a67bc717c408 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:31:37 +0100
Subject: Deactivate implicit arguments in printing notations bound to "@f".

This is to match the parsing policy (see #11091).

In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
---
 interp/constrextern.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 681d6ba541..362fe83ffa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,9 +1211,14 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
-              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
-              let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
-              (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
+              let args2scopes =
+                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2impls =
+                if n = 0 then
+                  (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+                     conventionally deactivates implicit arguments *)
+                  []
+                else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
-- 
cgit v1.2.3


From 14196d8ab425f67faf3995bd29a003de3b2e87ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:26:14 +0100
Subject: Propagate implicit arguments in all notations for partial
 applications.

This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cfd50e26e..e14629df9b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2070,9 +2070,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) ->
                intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (_,ntn,([],[],[],[])) ->
+            | CNotation (_,ntn,ntnargs) ->
                 assert (Option.is_empty isproj);
-                let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
+                let c = intern_notation intern env ntnvars loc ntn ntnargs in
                 let x, impl, scopes, l = find_appl_head_data c in
                   (x,impl,scopes,l), args
             | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
-- 
cgit v1.2.3


From 04b9870f0ebe79fde789551c8e172aad1e7cfc5c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:52:01 +0100
Subject: Inherit argument scopes in notations to expressions of the form @f.

This is a change of semantics.
---
 interp/constrextern.ml | 3 +--
 interp/constrintern.ml | 4 ++--
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 362fe83ffa..7f5f03610b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,8 +1211,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
-              let args2scopes =
-                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls =
                 if n = 0 then
                   (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e14629df9b..1149cf1f58 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1071,11 +1071,11 @@ let find_appl_head_data c =
       c, impls, scopes, []
   | GApp (r, l) ->
     begin match DAst.get r with
-    | GRef (ref,_) when l != [] ->
+    | GRef (ref,_) ->
       let n = List.length l in
       let impls = implicits_of_global ref in
       let scopes = find_arguments_scope ref in
-        c, List.map (drop_first_implicits n) impls,
+        c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
         List.skipn_at_least n scopes,[]
     | _ -> c,[],[],[]
     end
-- 
cgit v1.2.3


From ba52fd0dff4dcf06621fb91ff4902a060a0b222d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 11:36:51 +0100
Subject: Use auxiliary function for externing record patterns.

Also apply the same conditions for printing constructors as record
instances in both terms and patterns.
---
 interp/constrextern.ml | 54 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 33 insertions(+), 21 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7f5f03610b..c68a60fc93 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -403,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
+let extern_record_pattern cstrsp args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let projs = Recordops.lookup_projections (fst cstrsp) in
+    if PrintingRecord.active (fst cstrsp) then
+      ()
+    else if PrintingConstructor.active (fst cstrsp) then
+      raise Exit
+    else if not (get_record_print ()) then
+      raise Exit;
+    let rec ip projs args acc =
+      match projs, args with
+      | [], [] -> acc
+      | proj :: q, pat :: tail ->
+        let acc =
+          match proj, pat with
+          | _, { CAst.v = CPatAtom None } ->
+            (* we don't want to have 'x := _' in our patterns *)
+            acc
+          | Some c, _ ->
+            let loc = pat.CAst.loc in
+            (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc
+          | _ -> raise No_match in
+        ip q tail acc
+      | _ -> assert false
+    in
+    Some (List.rev (ip projs args []))
+  with
+    Not_found | No_match | Exit -> None
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
@@ -437,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
         | PatCstr(cstrsp,args,na) ->
           let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
           let p =
-            try
-              if !Flags.raw_print then raise Exit;
-              let projs = Recordops.lookup_projections (fst cstrsp) in
-              let rec ip projs args acc =
-                match projs, args with
-                  | [], [] -> acc
-                  | proj :: q, pat :: tail ->
-                     let acc =
-                       match proj, pat with
-                       | _, { CAst.v = CPatAtom None } ->
-                          (* we don't want to have 'x := _' in our patterns *)
-                          acc
-                       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
-                       | _ -> raise No_match in
-                     ip q tail acc
-                  | _ -> assert false
-              in
-              CPatRecord(List.rev (ip projs args []))
-            with
-                Not_found | No_match | Exit ->
+            match extern_record_pattern cstrsp args with
+            | Some l -> CPatRecord l
+            | None ->
                   let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
                     if pattern_printable_in_both_syntax cstrsp
-- 
cgit v1.2.3


From 3eea1e383e23ea76fcd49a7b302f31b2e3f6ef2a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:14:37 +0100
Subject: Fix inheritance of argument scopes when printing notations in
 patterns.

---
 interp/constrextern.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c68a60fc93..008e84cd9c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -508,7 +508,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
                 let subscope = (subentry,(scopt,scl@scopes')) in
                 List.map (extern_cases_pattern_in_scope subscope vars) c)
                 substlist in
-            let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+            let subscopes = find_arguments_scope gr in
+            let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+            let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+            let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
               else
                 match drop_implicits_in_patt gr nb_to_drop l2 with
@@ -528,7 +531,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
         List.rev_map (fun (c,(subentry,(scopt,scl))) ->
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
-      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+      let subscopes = find_arguments_scope gr in
+      let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+      let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+      let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
           match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
-- 
cgit v1.2.3


From 32467acf285629c28cbda27d27a8cf248150f2bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:44:44 +0100
Subject: Fix index bug in computing implicit signature of abbrev. in pattern
 printing.

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 008e84cd9c..b05ca8e5a6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -537,7 +537,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+          match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in
-- 
cgit v1.2.3


From 8d80875d230bd8af5611ec04bced1e5a17d058b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:46:42 +0100
Subject: Inherit scopes and implicit sign. in notations for partially applied
 pattern.

Exception: when the notation is to some @id.

Formerly, this was ignored for all kinds of string notations.
---
 interp/constrintern.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1149cf1f58..1b9b45c3fb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1680,7 +1680,7 @@ let drop_notations_pattern looked_for genv =
           test_kind top g;
           Dumpglob.add_glob ?loc:qid.loc g;
           let (_,argscs) = find_remaining_scopes [] pats g in
-          Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
+          Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
     with Not_found -> None
   and in_pat top scopes pt =
     let open CAst in
@@ -1780,7 +1780,15 @@ let drop_notations_pattern looked_for genv =
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
       let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
-      DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
+      let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in
+      let pat =
+        if List.length pl = 0 then
+          (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+             implicit arguments are not inherited *)
+          RCPatCstr (g, pl @ args, [])
+        else
+          RCPatCstr (g, pl, args) in
+      DAst.make ?loc @@ pat
     | NList (x,y,iter,terminator,revert) ->
       if not (List.is_empty args) then user_err ?loc
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
-- 
cgit v1.2.3


From 9da7715108554a5105c012685e90b2fa563abf08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:41:00 +0100
Subject: In printing patterns, distinguish the case of a notation to @id.

This is a case which conventionally deactivates implicit arguments.
---
 interp/constrextern.ml  |  8 +++++---
 interp/notation_ops.ml  | 21 ++++++++++++---------
 interp/notation_ops.mli |  4 ++--
 3 files changed, 19 insertions(+), 14 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b05ca8e5a6..4ec9f17c71 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -485,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       in
       insert_pat_coercion coercion pat
 
-and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args))
     (custom, (tmp_scope, scopes) as allscopes) vars =
   function
     | NotationRule (_,ntn as specific_ntn) ->
@@ -514,7 +514,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
             let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
               else
-                match drop_implicits_in_patt gr nb_to_drop l2 with
+                if no_implicit then l2 else
+                  match drop_implicits_in_patt gr nb_to_drop l2 with
                   |Some true_args -> true_args
                   |None -> raise No_match
             in
@@ -537,7 +538,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr nb_to_drop l2 with
+          if no_implicit then l2 else
+            match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d1eb50d370..59a58d643c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
 
 let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
-  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
-  | PatVar Anonymous, NHole _ -> sigma,(0,[])
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
+  | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
-      sigma,(0,l)
+      sigma,(false,0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
-      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
+      if le2 > List.length l1
       then
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 l1 in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        (* Convention: notations to @f don't keep implicit arguments *)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      | out,(_,[]) -> out
+      | out,(_,_,[]) -> out
       | _ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
   | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
-      sigma,(0,pats)
+      sigma,(false,0,pats)
   | NApp (NRef (GlobRef.IndRef r2),l2)
       when eq_ind ind r2 ->
       let le2 = List.length l2 in
@@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 =
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 pats in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   |_ -> raise No_match
 
 let reorder_canonically_substitution terms termlists metas =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c62dac013b..2ab8b620df 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)
 
-- 
cgit v1.2.3


From a905e70df85ef7bf700bb3d6a1b48ae180dfa987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:42:35 +0100
Subject: Inherit arguments scopes in pattern notations bound to some @id.

---
 interp/constrintern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1b9b45c3fb..f68f4e67b9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,10 +1659,11 @@ let drop_notations_pattern looked_for genv =
           let () = assert (List.is_empty vars) in
           let (_,argscs) = find_remaining_scopes [] pats g in
           Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
-        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
               test_kind top g;
               let () = assert (List.is_empty vars) in
-              Some (g, List.map (in_pat false scopes) pats, [])
+              let (_,argscs) = find_remaining_scopes [] pats g in
+              Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
         | NApp (NRef g,args) ->
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
               test_kind top g;
-- 
cgit v1.2.3


From bf1e15181a2531a106fa643ca8e9233cb889af12 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Nov 2019 21:49:47 +0100
Subject: Fixes #4690: do not allow @f in notations when f is a notation
 variable.

---
 interp/constrintern.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f68f4e67b9..c39e61083d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
+let check_not_notation_variable f ntnvars =
+  (* Check bug #4690 *)
+  match DAst.get f with
+  | GVar id when Id.Map.mem id ntnvars ->
+    user_err (str "Prefix @ is not applicable to notation variables.")
+  | _ ->
+     ()
+
 let option_mem_assoc id = function
   | Some (id',c) -> Id.equal id id'
   | None -> false
@@ -2063,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
             lvar us args ref
         in
+        check_not_notation_variable f ntnvars;
         (* Rem: GApp(_,f,[]) stands for @f *)
         if args = [] then DAst.make ?loc @@ GApp (f,[]) else
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
-- 
cgit v1.2.3