From c8c93bfea6e3c75ebce256f44043a34fe8933b5e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Apr 2020 00:50:06 +0200
Subject: 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.
---
 interp/constrintern.ml | 363 +++++++++++++++++++++----------------------------
 1 file changed, 156 insertions(+), 207 deletions(-)

(limited to 'interp')

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 ()
 
-- 
cgit v1.2.3