Fixing support for argument scopes and let-ins while interning cases patterns.

We also simplify the whole process of interpretation of cases pattern
on the way.

8 files changed, 349 insertions, 232 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index aee571131e..c23536edd5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1230,6 +1230,37 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       in
       c, None, args2
 
+let intern_qualid_for_pattern test_global intern_not qid pats =
+  match intern_extended_global_of_qualid qid with
+  | TrueGlobal g ->
+    test_global g;
+    (g, false, Some [], pats)
+  | SynDef kn ->
+    let filter (vars,a) =
+      match a with
+      | NRef g ->
+        (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
+        test_global g;
+        let () = assert (List.is_empty vars) in
+        Some (g, Some [], pats)
+      | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
+        test_global g;
+        let () = assert (List.is_empty vars) in
+        Some (g, None, pats)
+      | NApp (NRef g,args) ->
+        (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
+        test_global g;
+        let nvars = List.length vars in
+        if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
+        let pats1,pats2 = List.chop nvars pats in
+        let subst = split_by_type_pat vars (pats1,[]) in
+        let args = List.map (intern_not subst) args in
+        Some (g, Some args, pats2)
+      | _ -> None in
+    match Syntax_def.search_filtered_syntactic_definition filter kn with
+    | Some (g, pats1, pats2) -> (g, true, pats1, pats2)
+    | None -> raise Not_found
+
 let warn_nonprimitive_projection =
   CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled
     Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
@@ -1300,9 +1331,7 @@ let interp_reference vars r =
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
   | RCPatAlias of 'a raw_cases_pattern_expr * lname
-  | RCPatCstr  of GlobRef.t
-    * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
-  (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
+  | RCPatCstr  of GlobRef.t * 'a raw_cases_pattern_expr list
   | RCPatAtom  of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
   | RCPatOr    of 'a raw_cases_pattern_expr list
 and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1320,22 +1349,19 @@ let rec simple_adjust_scopes n scopes =
   | [] -> None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
-let find_remaining_scopes pl1 pl2 ref =
-  let impls_st = implicits_of_global ref in
-  let len_pl1 = List.length pl1 in
-  let len_pl2 = List.length pl2 in
-  let impl_list = if Int.equal len_pl1 0
-    then select_impargs_size len_pl2 impls_st
-    else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
-  let allscs = find_arguments_scope ref in
-  let scope_list = List.skipn_at_least len_pl1 allscs in
-  let rec aux = function
-    |[],l -> l
-    |_,[] -> []
-    |h::t,_::tt when is_status_implicit h -> aux (t,tt)
-    |_::t,h::tt -> h :: aux (t,tt)
-  in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
-      simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
+let rec adjust_to_up l l' default =
+  match l, l' with
+  | l, [] -> []
+  | [], l -> l
+  | true::l, l' -> default :: adjust_to_up l l' default
+  | false::l, y::l' -> y :: adjust_to_up l l' default
+
+let rec adjust_to_down l l' default =
+  match l, l' with
+  | [], l -> []
+  | true::l, l' -> adjust_to_down l l' default
+  | false::l, [] -> default :: adjust_to_down l [] default
+  | false::l, y::l' -> y :: adjust_to_down l l' default
 
 (* @return the first variable that occurs twice in a pattern
 
@@ -1378,76 +1404,16 @@ let check_or_pat_variables loc ids idsl =
        Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).")
   | [] -> ()
 
-open Declarations
-
-(* Similar to Cases.adjust_local_defs but on RCPat *)
-let insert_local_defs_in_pattern (ind,j) l =
-  let (mib,mip) = Global.lookup_inductive ind in
-  if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
-    (* Optimisation *) l
-  else
-    let (ctx, _) = mip.mind_nf_lc.(j-1) in
-    let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
-    let rec aux decls args =
-      match decls, args with
-      | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args
-      | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
-      | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
-      | _ -> assert false in
-    aux decls l
-
-let add_local_defs_and_check_length loc env g pl args =
-  let open GlobRef in
-  match g with
-  | ConstructRef cstr ->
-     (* We consider that no variables corresponding to local binders
-        have been given in the "explicit" arguments, which come from a
-        "@C args" notation or from a custom user notation *)
-     let pl' = insert_local_defs_in_pattern cstr pl in
-     let maxargs = Inductiveops.constructor_nalldecls env cstr in
-     if List.length pl' + List.length args > maxargs then
-       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
-     (* Two possibilities: either the args are given with explicit
-     variables for local definitions, then we give the explicit args
-     extended with local defs, so that there is nothing more to be
-     added later on; or the args are not enough to have all arguments,
-     which a priori means local defs to add in the [args] part, so we
-     postpone the insertion of local defs in the explicit args *)
-     (* Note: further checks done later by check_constructor_length *)
-     if List.length pl' + List.length args = maxargs then pl' else pl
-  | _ -> pl
-
-let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
-  let impl_list = if Int.equal len_pl1 0
-    then select_impargs_size (List.length pl2) impls_st
-    else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
-  let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
-  let rec aux i = function
-    |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
-             ((if Int.equal args_len nargs then false
-              else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
-               ,l)
-    |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out)
-      else fail (remaining_args (len_pl1+i) il)
-    |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom None)::out)
-      else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
-  in aux 0 (impl_list,pl2)
-
-let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
-  let nargs = Inductiveops.constructor_nallargs env c in
-  let nargs' = Inductiveops.constructor_nalldecls env c in
-  let impls_st = implicits_of_global (GlobRef.ConstructRef c) in
-  add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
-    nargs nargs' impls_st len_pl1 pl2
-
-let add_implicits_check_ind_length env loc c len_pl1 pl2 =
-  let nallargs = inductive_nallargs env c in
-  let nalldecls = inductive_nalldecls env c in
-  let impls_st = implicits_of_global (GlobRef.IndRef c) in
-  add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
-    nallargs nalldecls impls_st len_pl1 pl2
+let check_has_letin ?loc g expanded nargs nimps tags =
+  let expected_ndecls = List.length tags - nimps in
+  let expected_nassums = List.count (fun x -> not x) tags - nimps in
+  if nargs = expected_nassums then false
+  else if nargs = expected_ndecls then true else
+    let env = Global.env() in
+    match g with
+    | GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env cstr expanded nargs expected_nassums expected_ndecls
+    | GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ind expanded nargs expected_nassums expected_ndecls
+    | _ -> assert false
 
 (** Do not raise NotEnoughArguments thanks to preconditions*)
 let chop_params_pattern loc ind args with_letin =
@@ -1634,9 +1600,8 @@ let product_of_cases_patterns aliases idspl =
 let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatAtom id as p ->
     begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end
-  | RCPatCstr (id,l1,l2) ->
-    RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
-               List.map (subst_pat_iterator y t) l2)
+  | RCPatCstr (id,l) ->
+    RCPatCstr (id,List.map (subst_pat_iterator y t) l)
   | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
   | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
@@ -1653,10 +1618,15 @@ let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
     ~key:["Asymmetric";"Patterns"]
     ~value:false
 
+type global_reference_test = {
+  for_ind : bool;
+  test_kind : ?loc:Loc.t -> GlobRef.t -> unit
+}
+
 let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
-  let ensure_kind test_kind ?loc g =
+  let ensure_kind {test_kind} ?loc g =
     try test_kind ?loc g
     with Not_found ->
       error_invalid_pattern_notation ?loc ()
@@ -1664,83 +1634,47 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
   (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
   let rec rcp_of_glob scopes x = DAst.(map (function
     | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
-    | GHole (_,_,_) -> RCPatAtom (None)
-    | GRef (g,_) -> RCPatCstr (g,[],[])
+    | GHole (_,_,_) -> RCPatAtom None
+    | GRef (g,_) -> RCPatCstr (g, [])
     | GApp (r, l) ->
       begin match DAst.get r with
       | GRef (g,_) ->
         let allscs = find_arguments_scope g in
-        let allscs = simple_adjust_scopes (List.length l) allscs in (* TO CHECK *)
-        RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l,[])
+        let allscs = simple_adjust_scopes (List.length l) allscs in
+        RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l)
       | _ ->
         CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.")
       end
     | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
   in
-  let add_pars ?loc g syndef_pl pl =
-    (* Asymmetric compatibility mode *)
-    if get_asymmetric_patterns () then
-      let expl_pl =
-        if syndef_pl = [] then
-          let env = Global.env () in
-          let n = match g with
-            | GlobRef.ConstructRef (ind,_ as cstr) ->
-              let n = List.length pl in
-              if Int.equal n (Inductiveops.constructor_nrealargs env cstr) then
-                Inductiveops.inductive_nparams env ind
-              else if Int.equal n (Inductiveops.constructor_nrealdecls env cstr) then
-                Inductiveops.inductive_nparamdecls env ind
-              else
-                error_wrong_numarg_constructor ?loc env cstr
-                  (Inductiveops.constructor_nrealargs env cstr)
-            | _ -> 0 in
-          List.make n (DAst.make @@ RCPatAtom None)
-        else
-          syndef_pl in
-      expl_pl @ pl, []
-    else
-      syndef_pl, pl in
-  let rec drop_syndef test_kind ?loc scopes qid pats =
+  let make_pars ?loc g =
+    let env = Global.env () in
+    let n = match g with
+      | GlobRef.ConstructRef (ind,_) -> Inductiveops.inductive_nparams env ind
+      | _ -> 0 in
+    List.make n (DAst.make ?loc @@ RCPatAtom None)
+  in
+  let rec drop_syndef {test_kind} ?loc scopes qid add_par_if_no_ntn_with_par no_impl pats =
     try
-      if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then
+      if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids && List.is_empty pats then
         raise Not_found;
-      match Nametab.locate_extended qid with
-      | SynDef sp ->
-        let filter (vars,a) =
-        try match a with
-        | NRef g ->
-          (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
-          test_kind ?loc g;
-          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 deactivates implicit arguments *)
-              test_kind ?loc g;
-              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,args) ->
-              (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
-              test_kind ?loc g;
-              let nvars = List.length vars in
-              if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
-              let pats1,pats2 = List.chop nvars pats in
-              let subst = split_by_type_pat vars (pats1,[]) in
-              let idspl1 = List.map (in_not test_kind_inner qid.loc scopes subst []) args in
-              let (_,argscs) = find_remaining_scopes pats1 pats2 g in
-              Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
-        | _ -> raise Not_found
-        with Not_found -> None in
-        Syntax_def.search_filtered_syntactic_definition filter sp
-      | TrueGlobal g ->
-          test_kind ?loc g;
-          Dumpglob.add_glob ?loc:qid.loc g;
-          let (_,argscs) = find_remaining_scopes [] pats g in
-          Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
+      let intern_not subst pat = in_not test_kind_inner qid.loc scopes subst [] pat in
+      let g, expanded, ntnpats, pats = intern_qualid_for_pattern (test_kind ?loc) intern_not qid pats in
+      match ntnpats with
+      | None ->
+        (* deactivate implicit *)
+        let ntnpats = if add_par_if_no_ntn_with_par then make_pars ?loc g else [] in
+        Some (g, in_patargs ?loc scopes g expanded true ntnpats pats)
+      | Some ntnpats ->
+        let ntnpats = if add_par_if_no_ntn_with_par && ntnpats = [] then make_pars ?loc g else ntnpats in
+        Some (g, in_patargs ?loc scopes g expanded no_impl ntnpats pats)
     with Not_found -> None
-  and in_pat test_kind scopes pt =
+  and in_pat ({for_ind} as test_kind) scopes pt =
     let open CAst in
     let loc = pt.loc in
+    (* The two policies implied by asymmetric pattern mode *)
+    let add_par_if_no_ntn_with_par = get_asymmetric_patterns () && not for_ind in
+    let no_impl = get_asymmetric_patterns () && not for_ind in
     match pt.v with
     | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id)
     | CPatRecord l ->
@@ -1749,29 +1683,21 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
       begin match sorted_fields with
         | None -> DAst.make ?loc @@ RCPatAtom None
         | Some (n, head, pl) ->
-          let pl =
-            let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
-            List.rev_append pars pl
-          in
-          let (_,argscs) = find_remaining_scopes [] pl head in
-          let pats = List.map2 (in_pat_sc scopes) argscs pl in
-          DAst.make ?loc @@ RCPatCstr(head, pats, [])
+          let pars = make_pars ?loc head in
+          let pats = in_patargs ?loc scopes head true true pars pl in
+          DAst.make ?loc @@ RCPatCstr(head, pats)
       end
     | CPatCstr (head, None, pl) ->
       begin
-        match drop_syndef test_kind ?loc scopes head pl with
-        | Some (g,syndef_pl,pl) ->
-          let expl_pl, pl_wo_impl = add_pars ?loc g syndef_pl pl in
-          DAst.make ?loc @@ RCPatCstr(g, expl_pl, pl_wo_impl)
-        | None ->
-          Loc.raise ?loc (InternalizationError (NotAConstructor head))
+        match drop_syndef test_kind ?loc scopes head add_par_if_no_ntn_with_par no_impl pl with
+        | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr(g, pl)
+        | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
       end
     | CPatCstr (qid, Some expl_pl, pl) ->
       begin
-        match drop_syndef test_kind scopes qid expl_pl with
+        match drop_syndef test_kind ?loc scopes qid false true (expl_pl@pl) with
+        | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr (g, pl)
         | None -> Loc.raise ?loc (InternalizationError (NotAConstructor qid))
-        | Some (g,syndef_pl,extra_expl_pl) ->
-          DAst.make ?loc @@ RCPatCstr (g, syndef_pl @ extra_expl_pl @ List.map (in_pat test_kind_inner scopes) pl, [])
       end
     | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in
@@ -1788,23 +1714,20 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
     | CPatDelimiters (key, e) ->
       in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e
     | CPatPrim p ->
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner.test_kind p scopes in
       rcp_of_glob scopes pat
     | CPatAtom (Some id) ->
       begin
-        match drop_syndef test_kind ?loc scopes id [] with
-          | Some (g,syndef_pl,empty_pl) ->
-            let expl_pl, pl_wo_impl = add_pars ?loc g syndef_pl empty_pl in
-            DAst.make ?loc @@ RCPatCstr (g, expl_pl, pl_wo_impl)
-          | None ->
-            DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
+        match drop_syndef test_kind ?loc scopes id add_par_if_no_ntn_with_par no_impl [] with
+        | Some (g, pl) -> DAst.make ?loc @@ RCPatCstr (g, pl)
+        | None         -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
       end
     | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
     | CPatOr pl     -> DAst.make ?loc @@ RCPatOr (List.map (in_pat test_kind scopes) pl)
     | CPatCast (_,_) ->
       (* We raise an error if the pattern contains a cast, due to
          current restrictions on casts in patterns. Cast in patterns
-         are supported only in local binders and only at top level.
+         are supported only in local binders and only at for_ind level.
          The only reason they are in the [cases_pattern_expr] type
          is that the parser needs to factor the "c : t" notation
          with user defined notations. In the long term, we will try to
@@ -1814,7 +1737,40 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
          duplicating the levels of the [pattern] rule. *)
       CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
   and in_pat_sc scopes x = in_pat test_kind_inner (x,snd scopes)
-  and in_not (test_kind:?loc:Loc.t->'a->'b) loc scopes (subst,substlist as fullsubst) args = function
+  and in_patargs ?loc scopes g expanded no_impl ntnpats pats =
+    let default = DAst.make ?loc @@ RCPatAtom None in
+    let npats = List.length pats in
+    let n = List.length ntnpats in
+    let ntnpats_with_letin, tags =
+      let tags = match g with
+      | GlobRef.ConstructRef cstr -> constructor_alltags (Global.env()) cstr
+      | GlobRef.IndRef ind -> inductive_alltags (Global.env()) ind
+      | _ -> assert false in
+      let ntnpats_with_letin = adjust_to_up tags ntnpats default in
+      ntnpats_with_letin, List.skipn (List.length ntnpats_with_letin) tags in
+    let imps =
+      let imps =
+        if no_impl then [] else
+          let impls_st = implicits_of_global g in
+          if Int.equal n 0 then select_impargs_size npats impls_st
+          else List.skipn_at_least n (select_stronger_impargs impls_st) in
+      adjust_to_down tags imps None in
+    let subscopes = adjust_to_down tags (List.skipn_at_least n (find_arguments_scope g)) None in
+    let has_letin = check_has_letin ?loc g expanded npats (List.count is_status_implicit imps) tags in
+    let rec aux imps subscopes tags pats =
+    match imps, subscopes, tags, pats with
+    | _, _, true::tags, p::pats when has_letin ->
+      in_pat_sc scopes None p :: aux imps subscopes tags pats
+    | _, _, true::tags, _ ->
+      default :: aux imps subscopes tags pats
+    | imp::imps, sc::subscopes, false::tags, _ when is_status_implicit imp ->
+      default :: aux imps subscopes tags pats
+    | imp::imps, sc::subscopes, false::tags, p::pats ->
+      in_pat_sc scopes sc p :: aux imps subscopes tags pats
+    | _, _, [], [] -> []
+    | _ -> assert false in
+    ntnpats_with_letin @ aux imps subscopes tags pats
+  and in_not test_kind loc scopes (subst,substlist as fullsubst) args = function
     | NVar id ->
       let () = assert (List.is_empty args) in
       begin
@@ -1829,22 +1785,15 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
       end
     | NRef g ->
       ensure_kind test_kind ?loc g;
-      let (_,argscs) = find_remaining_scopes [] args g in
-      DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
-    | NApp (NRef g,pl) ->
+      DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true false [] args)
+    | NApp (NRef g,ntnpl) ->
       ensure_kind test_kind ?loc g;
-      let (_,argscs2) = find_remaining_scopes pl args g in
-      let pl = List.map (in_not test_kind_inner loc scopes fullsubst []) pl in
-      let pl = add_local_defs_and_check_length loc genv g pl args in
-      let args = List.map2 (fun x -> in_pat test_kind_inner (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
+      let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in
+      let no_impl =
+        (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+           implicit arguments are not inherited *)
+        ntnpl = [] in
+      DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true no_impl ntnpl args)
     | 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.");
@@ -1877,10 +1826,9 @@ let rec intern_pat genv ntnvars aliases pat =
     | RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat genv ntnvars aliases' p
-    | RCPatCstr (head, expl_pl, pl) ->
+    | RCPatCstr (head, pl) ->
       let c = find_constructor loc head in
-      let with_letin, pl2 = add_implicits_check_constructor_length genv loc c (List.length expl_pl) pl in
-      intern_cstr_with_all_args loc c with_letin [] (expl_pl@pl2)
+      intern_cstr_with_all_args loc c true [] pl
     | RCPatAtom (Some ({loc;v=id},scopes)) ->
       let aliases = merge_aliases aliases (make ?loc @@ Name id) in
       set_var_scope ?loc id false scopes ntnvars;
@@ -1897,8 +1845,9 @@ let rec intern_pat genv ntnvars aliases pat =
       (ids,List.flatten pl')
 
 let intern_cases_pattern test_kind genv ntnvars env aliases pat =
+  let test = {for_ind=false;test_kind} in
   intern_pat genv ntnvars aliases
-    (drop_notations_pattern (test_kind,test_kind) genv env pat)
+    (drop_notations_pattern (test,test) genv env pat)
 
 let _ =
   intern_cases_pattern_fwd :=
@@ -1918,21 +1867,21 @@ let intern_ind_pattern genv ntnvars env pat =
       raise Not_found in
   let no_not =
     try
-      drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat
+      let test_top = {for_ind=true;test_kind=test_kind_top} in
+      let test_inner = {for_ind=false;test_kind=test_kind_inner} in
+      drop_notations_pattern (test_top,test_inner) genv env pat
     with InternalizationError (NotAConstructor _) as exn ->
       let _, info = Exninfo.capture exn in
       error_bad_inductive_type ~info ()
   in
   let loc = no_not.CAst.loc in
   match DAst.get no_not with
-    | RCPatCstr (head, expl_pl, pl) ->
+    | RCPatCstr (head, pl) ->
       let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc ()) head in
-      let with_letin, pl2 = add_implicits_check_ind_length genv loc c
-        (List.length expl_pl) pl in
-      let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
-      (with_letin,
+      let idslpl = List.map (intern_pat genv ntnvars empty_alias) pl in
+      (true,
        match product_of_cases_patterns empty_alias idslpl with
-       | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
+       | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl true)
        | _ -> error_bad_inductive_type ?loc ())
     | x -> error_bad_inductive_type ?loc ()
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a793e217d4..14417d15c6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -46,8 +46,8 @@ module NamedDecl = Context.Named.Declaration
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of constructor * bool * int * int * int
+  | WrongNumargInductive of inductive * bool * int * int * int
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
@@ -65,11 +65,11 @@ let error_bad_constructor ?loc env cstr ind =
   raise_pattern_matching_error ?loc
     (env, Evd.empty, BadConstructor (cstr,ind))
 
-let error_wrong_numarg_constructor ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n))
+let error_wrong_numarg_constructor ?loc env c expanded n n1 n2 =
+  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,expanded,n,n1,n2))
 
-let error_wrong_numarg_inductive ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))
+let error_wrong_numarg_inductive ?loc env c expanded n n1 n2 =
+  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,expanded,n,n1,n2))
 
 let list_try_compile f l =
   let rec aux errors = function
@@ -519,13 +519,17 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
         (* Check the constructor has the right number of args *)
         let ci = cstrs.(i-1) in
         let nb_args_constr = ci.cs_nargs in
-        if Int.equal (List.length args) nb_args_constr then pat
+        let nargs = List.length args in
+        if Int.equal nargs nb_args_constr then pat
         else
           try
             let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
             in DAst.make ?loc @@ PatCstr (cstr, args', alias)
           with NotAdjustable ->
-            error_wrong_numarg_constructor ?loc env cstr nb_args_constr
+            let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in
+            (* In practice, this is already checked at interning *)
+            error_wrong_numarg_constructor ?loc env cstr
+              (* as if not expanded: *) false nargs nb_args_constr (nb_args_constr + nlet)
       else
         (* Try to insert a coercion *)
         try
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9a986bc14c..10fd085e3a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,17 +23,17 @@ open Evardefine
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of constructor * bool * int * int * int
+  | WrongNumargInductive of inductive * bool * int * int * int
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> bool -> int -> int -> int -> 'a
 
-val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> bool -> int -> int -> int -> 'a
 
 val irrefutable : env -> cases_pattern -> bool
 
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 01564e7f25..984ac4e527 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -74,7 +74,9 @@ fun '{{n, m, p}} => n + m + p
 fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
-The constructor D (in type J) expects 3 arguments.
+Once notations are expanded, the resulting constructor D (in type J) is
+expected to be applied to no arguments while it is actually applied to
+1 argument.
 lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
@@ -181,3 +183,51 @@ end
 File "stdin", line 253, characters 4-5:
 Warning: Unused variable B catches more than one case.
 [unused-pattern-matching-variable,pattern-matching]
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 4 arguments (or
+6 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => n + p
+end
+     : J' bool (true, true) -> nat
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 2 arguments.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => (n, p)
+end
+     : J' bool (true, true) -> nat * nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 2d8a8b359c..0cb3ac3ddc 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -254,3 +254,33 @@ Definition bar (f : foo) :=
   end.
 
 End Wish12762.
+
+Module ConstructorArgumentsNumber.
+
+Arguments cons {A} _ _.
+
+Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c.
+
+Unset Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+(* Missing a let-in to be in let-in mode *)
+Fail Check fun x => match x with D' _ _ n p e => 0 end.
+Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end.
+Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end.
+
+Set Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+Fail Check fun x => match x with D' n _ => 0 end.
+Fail Check fun x => match x with D' n m p e _ => 0 end.
+Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end.
+Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
+
+End ConstructorArgumentsNumber.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 465b3eb8c0..90c1b308f2 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -89,3 +89,16 @@ Check fun x:Ind bool nat =>
   match x in Ind _ X Y Z return Z with
   | y => (true,0)
   end.
+
+(* A check that multi-implicit arguments work *)
+
+Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end.
+Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.
+
+(* Check that Asymmetric Patterns does not apply to the in clause *)
+
+Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
+Set Asymmetric Patterns.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
+Unset Asymmetric Patterns.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 232ac17cbf..e678fc7882 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1882,3 +1882,60 @@ Check match O in nat return nat with O => O | _ => O end.
 (* Checking that aliases are substituted in the correct order *)
 
 Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.
+
+(* Checking use of argument scopes *)
+
+Module Intern.
+
+Inductive I (A:Type) := C : nat -> let a:=0 in bool -> list bool -> bool -> I A.
+
+Close Scope nat_scope.
+Notation "0" := true : bool_scope.
+Notation "0" := nil : list_scope.
+Notation C' := @C (only parsing).
+Notation C'' := C (only parsing).
+Notation C''' := (C _ 0) (only parsing).
+
+Set Asymmetric Patterns.
+
+Check fun x => match x with C 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+
+Check fun x => match x with C' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C'' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C'' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C''' 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C''' _ 0 0 0 => O | _ => O end. (* was not supported  *)
+
+Unset Asymmetric Patterns.
+Arguments C {A} _ {x} _ _.
+
+Check fun x => match x with C 0 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C 0 _ 0 0 => O | _ => O end. (* was wrong scope on last argument with let-in *)
+
+Check fun x => match x with C' _ 0 _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C' _ 0 _ 0 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C'' _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C'' _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C''' 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C''' _ 0 0 => O | _ => O end. (* works by miscount compensating *)
+
+Check fun x => match x with (@C _ 0) _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C _ 0) _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with @C _ 0 _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with @C _ 0 _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with (@C) _ O _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C) _ O _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+End Intern.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d35e13c4ef..a38dfdb419 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1325,14 +1325,28 @@ let decline_string n s =
   else if Int.equal n 1 then str "1 " ++ str s
   else (int n ++ str " " ++ str s ++ str "s")
 
-let explain_wrong_numarg_constructor env cstr n =
-  str "The constructor " ++ pr_constructor env cstr ++
-  str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
-  str ") expects " ++ decline_string n "argument" ++ str "."
-
-let explain_wrong_numarg_inductive env ind n =
-  str "The inductive type " ++ pr_inductive env ind ++
-  str " expects " ++ decline_string n "argument" ++ str "."
+let explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp =
+  (if expanded then
+    strbrk "Once notations are expanded, the resulting "
+  else
+    strbrk "The ") ++ pp ++
+  strbrk " is expected to be applied to " ++ decline_string expected_nassums "argument" ++
+  (if expected_nassums = expected_ndecls then mt () else
+     strbrk " (or " ++ decline_string expected_ndecls "argument" ++
+     strbrk " when including variables for local definitions)") ++
+  strbrk " while it is actually applied to " ++
+  decline_string nargs "argument" ++ str "."
+
+let explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls =
+  let pp =
+    strbrk "constructor " ++ pr_constructor env cstr ++
+    strbrk " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
+    strbrk ")" in
+  explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
+
+let explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls =
+  let pp = strbrk "inductive type " ++ pr_inductive env ind in
+  explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
 
 let explain_unused_clause env pats =
   str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
@@ -1357,10 +1371,10 @@ let explain_pattern_matching_error env sigma = function
       explain_bad_pattern env sigma c t
   | BadConstructor (c,ind) ->
       explain_bad_constructor env c ind
-  | WrongNumargConstructor (c,n) ->
-      explain_wrong_numarg_constructor env c n
-  | WrongNumargInductive (c,n) ->
-      explain_wrong_numarg_inductive env c n
+  | WrongNumargConstructor (c,expanded,n,n1,n2) ->
+      explain_wrong_numarg_constructor env c expanded n n1 n2
+  | WrongNumargInductive (c,expanded,n,n1,n2) ->
+      explain_wrong_numarg_inductive env c expanded n n1 n2
   | UnusedClause tms ->
       explain_unused_clause env tms
   | NonExhaustive tms ->