Merge PR #12099: More parsing/printing notation/abbreviation consistency for mixed terms and pattern

Reviewed-by: ejgallego

6 files changed, 302 insertions, 89 deletions

diff --git a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst
new file mode 100644
index 0000000000..e9b02aed6d
--- /dev/null
+++ b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality)
+  (`#12099 <https://github.com/coq/coq/pull/12099>`_,
+  by Hugo Herbelin).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5fb6664dd6..409e46864e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -263,6 +263,13 @@ type intern_env = {
   binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option;
 }
 
+type pattern_intern_env = {
+  pat_scopes: Notation_term.subscopes;
+  (* ids = Some means accept local variables; this is useful for
+     terms as patterns parsed as pattersn in notations *)
+  pat_ids: Id.Set.t option;
+}
+
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
@@ -317,6 +324,9 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 let set_env_scopes env (scopt,subscopes) =
   {env with tmp_scope = scopt; scopes = subscopes @ env.scopes}
 
+let env_for_pattern env =
+  {pat_scopes = (env.tmp_scope, env.scopes); pat_ids = Some env.ids}
+
 let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body)
 let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 
@@ -420,6 +430,40 @@ let binder_status_fun = {
   slide = on_snd slide_binders;
 }
 
+(* [test_kind_strict] rules out pattern which refers to global other
+   than constructors or variables; It is used in instances of notations *)
+
+let test_kind_pattern_in_notation ?loc = function
+  | GlobRef.ConstructRef _ -> ()
+    (* We do not accept non constructors to be used as variables in
+       patterns *)
+  | GlobRef.ConstRef _ ->
+    user_err ?loc (str "Found a constant while a pattern was expected.")
+  | GlobRef.IndRef _ ->
+    user_err ?loc (str "Found an inductive type while a pattern was expected.")
+  | GlobRef.VarRef _ ->
+    (* we accept a section variable name to be used as pattern variable *)
+    raise Not_found
+
+let test_kind_ident_in_notation ?loc = function
+  | GlobRef.ConstructRef _ ->
+    user_err ?loc (str "Found a constructor while a variable name was expected.")
+  | GlobRef.ConstRef _ ->
+    user_err ?loc (str "Found a constant while a variable name was expected.")
+  | GlobRef.IndRef _ ->
+    user_err ?loc (str "Found an inductive type while a variable name was expected.")
+  | GlobRef.VarRef _ ->
+    (* we accept a section variable name to be used as pattern variable *)
+    raise Not_found
+
+(* [test_kind_tolerant] allow global reference names to be used as pattern variables *)
+
+let test_kind_tolerant ?loc = function
+  | GlobRef.ConstructRef _ -> ()
+  | GlobRef.ConstRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ ->
+    (* A non-constructor global reference in a pattern is seen as a variable *)
+    raise Not_found
+
 (**)
 
 let locate_if_hole ?loc na c = match DAst.get c with
@@ -539,9 +583,9 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
   (push_name_env ntnvars impls env locna,
    (na,Explicit,term,ty))
 
-let intern_cases_pattern_as_binder ?loc ntnvars env p =
+let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
   let il,disjpat =
-    let (il, subst_disjpat) = !intern_cases_pattern_fwd ntnvars (None,env.scopes) p in
+    let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in
     let substl,disjpat = List.split subst_disjpat in
     if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then
       user_err ?loc (str "Unsupported nested \"as\" clause.");
@@ -568,7 +612,7 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function
         | Some ty -> ty
         | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
       in
-      let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
+      let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
       let {v=(_,bk,t)} = List.hd bl' in
@@ -661,27 +705,21 @@ let is_patvar_store store pat =
   | PatVar na -> ignore(store na); true
   | _ -> false
 
-let out_patvar pat =
-  match pat.v with
+let out_patvar = CAst.map_with_loc (fun ?loc -> function
   | CPatAtom (Some qid) when qualid_is_ident qid ->
     Name (qualid_basename qid)
   | CPatAtom None -> Anonymous
-  | _ -> assert false
-
-let term_of_name = function
-  | Name id -> DAst.make (GVar id)
-  | Anonymous ->
-       let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-    DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None))
+  | _ -> assert false)
 
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
  | Anonymous -> (renaming,env), None, Anonymous
  | Name id ->
   let store,get = set_temporary_memory () in
+  let test_kind = test_kind_tolerant in
   try
     (* We instantiate binder name with patterns which may be parsed as terms *)
     let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
-    let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+    let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
     let pat, na = match disjpat with
     | [pat] when is_patvar_store store pat -> let na = get () in None, na
     | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
@@ -694,11 +732,11 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_patvar pat in
-      let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in
-      (renaming,env), None, na
+      let env = push_name_env ntnvars [] env na in
+      (renaming,env), None, na.v
     else
       (* Interpret as a pattern *)
-      let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+      let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
       let pat, na =
         match disjpat with
         | [pat] when is_patvar_store store pat -> let na = get () in None, na
@@ -829,22 +867,22 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       let arg = match arg with
       | None -> None
       | Some arg ->
-        let mk_env id (c, (tmp_scope, subscopes)) map =
-          let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
+        let mk_env id (c, scopes) map =
+          let nenv = set_env_scopes env scopes in
           try
             let gc = intern nenv c in
             Id.Map.add id (gc, None) map
           with Nametab.GlobalizationError _ -> map
         in
-        let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
-          let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
-          if onlyident then
-            let na = out_patvar c in term_of_name na, None
-          else
-            let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
-            match disjpat with
-            | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
-            | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
+        let mk_env' (c, (onlyident,scopes)) =
+          let nenv = set_env_scopes env scopes in
+          let test_kind =
+            if onlyident then test_kind_ident_in_notation
+            else test_kind_pattern_in_notation in
+          let _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in
+          match disjpat with
+          | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
+          | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
         let terms = Id.Map.fold mk_env terms Id.Map.empty in
         let binders = Id.Map.map mk_env' binders in
@@ -890,20 +928,19 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
     try
-      let (a,(scopt,subscopes)) = Id.Map.find id terms in
-      intern {env with tmp_scope = scopt;
-                scopes = subscopes @ env.scopes} a
+      let (a,scopes) = Id.Map.find id terms in
+      intern (set_env_scopes env scopes) a
     with Not_found ->
     try
       let pat,(onlyident,scopes) = Id.Map.find id binders in
-      let env = set_env_scopes env scopes in
-      if onlyident then
-        term_of_name (out_patvar pat)
-      else
-        let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
-        match disjpat with
-        | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
-        | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+      let nenv = set_env_scopes env scopes in
+      let test_kind =
+        if onlyident then test_kind_ident_in_notation
+        else test_kind_pattern_in_notation in
+      let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars nenv pat in
+      match disjpat with
+      | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
+      | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
     with Not_found ->
     try
       match binderopt with
@@ -1582,19 +1619,14 @@ let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
     ~key:["Asymmetric";"Patterns"]
     ~value:false
 
-let drop_notations_pattern looked_for genv =
+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 top loc g =
-    try
-      if top then looked_for g else
-      match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found
+  let ensure_kind test_kind ?loc g =
+    try test_kind ?loc g
     with Not_found ->
       error_invalid_pattern_notation ?loc ()
   in
-  let test_kind top =
-    if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found
-  in
   (* [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))
@@ -1611,47 +1643,49 @@ let drop_notations_pattern looked_for genv =
       end
     | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
   in
-  let rec drop_syndef top scopes qid pats =
+  let rec drop_syndef test_kind ?loc scopes qid pats =
     try
+      if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids 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 top g;
+          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 top g;
+              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 top g;
+              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 false qid.loc scopes subst []) args 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 top 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)
     with Not_found -> None
-  and in_pat top scopes pt =
+  and in_pat test_kind scopes pt =
     let open CAst in
     let loc = pt.loc in
     match pt.v with
-    | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
+    | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
         sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
@@ -1668,7 +1702,7 @@ let drop_notations_pattern looked_for genv =
       end
     | CPatCstr (head, None, pl) ->
       begin
-        match drop_syndef top scopes head pl with
+        match drop_syndef test_kind ?loc scopes head pl with
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
           | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
       end
@@ -1682,37 +1716,37 @@ let drop_notations_pattern looked_for genv =
       in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+        DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat test_kind_inner scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+        DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, [])
     | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Number (SMinus,p)) scopes in
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in
       rcp_of_glob scopes pat
     | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
-      in_pat top scopes a
+      in_pat test_kind scopes a
     | CPatNotation (_,ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
-      let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
+      let subst = split_by_type_pat ?loc ids' (terms,termlists) in
       Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
-      in_not top loc scopes (terms,termlists) extrargs c
+      in_not test_kind loc scopes subst extrargs c
     | CPatDelimiters (key, e) ->
-      in_pat top (None,find_delimiters_scope ?loc key::snd scopes) 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 false) p scopes in
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in
       rcp_of_glob scopes pat
     | CPatAtom (Some id) ->
       begin
-        match drop_syndef top scopes id [] with
+        match drop_syndef test_kind ?loc scopes id [] with
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
           | 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 top scopes) pl)
+    | 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
@@ -1725,8 +1759,8 @@ let drop_notations_pattern looked_for genv =
          This check is here and not in the parser because it would require
          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 false (x,snd scopes)
-  and in_not top loc scopes (subst,substlist as fullsubst) args = function
+  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
     | NVar id ->
       let () = assert (List.is_empty args) in
       begin
@@ -1734,21 +1768,21 @@ let drop_notations_pattern looked_for genv =
         (* of the notations *)
         try
           let (a,(scopt,subscopes)) = Id.Map.find id subst in
-          in_pat top (scopt,subscopes@snd scopes) a
+          in_pat test_kind (scopt,subscopes@snd scopes) a
         with Not_found ->
           if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
             anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
       end
     | NRef g ->
-      ensure_kind top loc 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) ->
-      ensure_kind top loc g;
+      ensure_kind test_kind ?loc g;
       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 = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
-      let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 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
@@ -1763,10 +1797,10 @@ let drop_notations_pattern looked_for genv =
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
          let (l,(scopt,subscopes)) = Id.Map.find x substlist in
-         let termin = in_not top loc scopes fullsubst [] terminator in
+         let termin = in_not test_kind_inner loc scopes fullsubst [] terminator in
          List.fold_right (fun a t ->
            let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
-           let u = in_not false loc scopes (nsubst, substlist) [] iter in
+           let u = in_not test_kind_inner loc scopes (nsubst, substlist) [] iter in
            subst_pat_iterator ldots_var t u)
            (if revert then List.rev l else l) termin
        with Not_found ->
@@ -1775,7 +1809,7 @@ let drop_notations_pattern looked_for genv =
       let () = assert (List.is_empty args) in
       DAst.make ?loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ?loc ()
-  in in_pat true
+  in in_pat test_kind_top env.pat_scopes pat
 
 let rec intern_pat genv ntnvars aliases pat =
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
@@ -1816,19 +1850,30 @@ let rec intern_pat genv ntnvars aliases pat =
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
-let intern_cases_pattern genv ntnvars scopes aliases pat =
+let intern_cases_pattern test_kind genv ntnvars env aliases pat =
   intern_pat genv ntnvars aliases
-    (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
+    (drop_notations_pattern (test_kind,test_kind) genv env pat)
 
 let _ =
   intern_cases_pattern_fwd :=
-    fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p
-
-let intern_ind_pattern genv ntnvars scopes pat =
+    fun test_kind ntnvars env p ->
+    intern_cases_pattern test_kind (Global.env ()) ntnvars env empty_alias p
+
+let intern_ind_pattern genv ntnvars env pat =
+  let test_kind_top ?loc = function
+    | GlobRef.IndRef _  -> ()
+    | GlobRef.ConstructRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ ->
+      (* A non-inductive global reference at top is an error *)
+      error_invalid_pattern_notation ?loc () in
+  let test_kind_inner ?loc = function
+    | GlobRef.ConstructRef _ -> ()
+    | GlobRef.IndRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ ->
+      (* A non-constructor global reference deep in a pattern is seen as a variable *)
+      raise Not_found in
   let no_not =
     try
-      drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
-    with InternalizationError(NotAConstructor _) as exn ->
+      drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat
+    with InternalizationError (NotAConstructor _) as exn ->
       let _, info = Exninfo.capture exn in
       error_bad_inductive_type ~info ()
   in
@@ -2221,7 +2266,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern env n pl =
-    let idsl_pll = List.map (intern_cases_pattern globalenv ntnvars (None,env.scopes) empty_alias) pl in
+    let env = { pat_ids = None; pat_scopes = (None,env.scopes) } in
+    let idsl_pll = List.map (intern_cases_pattern test_kind_tolerant globalenv ntnvars env empty_alias) pl in
     let loc = loc_of_multiple_pattern pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns empty_alias idsl_pll
@@ -2262,7 +2308,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     let match_td,typ = match t with
     | Some t ->
         let with_letin,(ind,ind_ids,alias_subst,l) =
-          intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
+          intern_ind_pattern globalenv ntnvars (env_for_pattern (set_type_scope env)) t in
         let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
         let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
         (* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -2403,7 +2449,8 @@ let intern_gen kind env sigma
 let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
 let intern_type env sigma c = intern_gen IsType env sigma c
 let intern_pattern globalenv patt =
-  intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
+  let env = {pat_ids = None; pat_scopes = (None, [])} in
+  intern_cases_pattern test_kind_tolerant globalenv Id.Map.empty env empty_alias patt
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 24b5dfce29..2e3fa0aa0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -941,7 +941,7 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
   try
     (* If already bound to a term, unify the binder and the term *)
     match DAst.get (Id.List.assoc var terms) with
-    | GVar id' ->
+    | GVar id' | GRef (GlobRef.VarRef id',None) ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
     | t ->
@@ -1147,16 +1147,22 @@ let does_not_come_from_already_eta_expanded_var glob =
   (* checked). *)
   match DAst.get glob with GVar _ -> false | _ -> true
 
+let is_var_term = function
+  (* The kind of expressions allowed to be both a term and a binding variable *)
+  | GVar _ -> true
+  | GRef (GlobRef.VarRef _,None) -> true
+  | _ -> false
+
 let rec match_ inner u alp metas sigma a1 a2 =
   let open CAst in
   let loc = a1.loc in
   match DAst.get a1, a2 with
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
-  | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
-  | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
-  | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_strict_meta id2 metas -> raise No_match
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index bdf3495479..f42c754ef5 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -523,6 +523,7 @@ let rec cases_pattern_of_glob_constr env na c =
     | Anonymous -> PatVar (Name id)
     end
   | GHole (_,_,_) -> PatVar na
+  | GRef (GlobRef.VarRef id,_) -> PatVar (Name id)
   | GRef (GlobRef.ConstructRef cstr,_) -> PatCstr (cstr,[],na)
   | GApp (c, l) ->
     begin match DAst.get c with
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index fa0c20bf73..a6fd39c29b 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -125,3 +125,57 @@ Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
      : Prop
 fun x : nat => <{ x; (S x) }>
      : nat -> nat
+exists p : nat, ▢_p (p >= 1)
+     : Prop
+▢_n (n >= 1)
+     : Prop
+The command has indeed failed with message:
+Found an inductive type while a variable name was expected.
+The command has indeed failed with message:
+Found a constructor while a variable name was expected.
+The command has indeed failed with message:
+Found a constant while a variable name was expected.
+exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
+     : Prop
+▢_n (n >= 1)
+     : Prop
+The command has indeed failed with message:
+Found an inductive type while a pattern was expected.
+▢_tt (tt = tt)
+     : Prop
+The command has indeed failed with message:
+Found a constant while a pattern was expected.
+exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
+     : Prop
+pseudo_force n (fun n : nat => n >= 1)
+     : Prop
+The command has indeed failed with message:
+Found an inductive type while a pattern was expected.
+▢_tt (tt = tt)
+     : Prop
+The command has indeed failed with message:
+Found a constant while a pattern was expected.
+exists x y : nat, myforce (x, y) (x >= 1 /\ y >= 2)
+     : Prop
+myforce n (n >= 1)
+     : Prop
+The command has indeed failed with message:
+Found an inductive type while a pattern was expected.
+myforce tt (tt = tt)
+     : Prop
+The command has indeed failed with message:
+Found a constant while a pattern was expected.
+id nat
+     : Set
+fun a : bool => id a
+     : bool -> bool
+fun nat : bool => id nat
+     : bool -> bool
+The command has indeed failed with message:
+Found an inductive type while a pattern was expected.
+!! nat, nat = true
+     : Prop
+!!! nat, nat = true
+     : Prop
+!!!! (nat, id), nat = true /\ id = false
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 84913abcdc..0731819bba 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -313,3 +313,104 @@ Notation "x" := x (in custom com_top at level 90, x custom com at level 90).
 Check fun x => <{ x ; (S x) }>.
 
 End CoercionEntryTransitivity.
+
+(* Some corner cases *)
+
+Module P.
+
+(* Basic rules:
+   - a section variable be used for itself and as a binding variable
+   - a global name cannot be used for itself and as a binding variable
+*)
+
+  Definition pseudo_force {A} (n:A) (P:A -> Prop) := forall n', n' = n -> P n'.
+
+  Module NotationMixedTermBinderAsIdent.
+
+  Notation "▢_ n P" := (pseudo_force n (fun n => P))
+    (at level 0, n ident, P at level 9, format "▢_ n  P").
+  Check exists p, ▢_p (p >= 1).
+  Section S.
+  Variable n:nat.
+  Check ▢_n (n >= 1).
+  End S.
+  Fail Check ▢_nat (nat = bool).
+  Fail Check ▢_O (O >= 1).
+  Axiom n:nat.
+  Fail Check ▢_n (n >= 1).
+
+  End NotationMixedTermBinderAsIdent.
+
+  Module NotationMixedTermBinderAsPattern.
+
+  Notation "▢_ n P" := (pseudo_force n (fun n => P))
+    (at level 0, n pattern, P at level 9, format "▢_ n  P").
+  Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2).
+  Section S.
+  Variable n:nat.
+  Check ▢_n (n >= 1).
+  End S.
+  Fail Check ▢_nat (nat = bool).
+  Check ▢_tt (tt = tt).
+  Axiom n:nat.
+  Fail Check ▢_n (n >= 1).
+
+  End NotationMixedTermBinderAsPattern.
+
+  Module NotationMixedTermBinderAsStrictPattern.
+
+  Notation "▢_ n P" := (pseudo_force n (fun n => P))
+    (at level 0, n strict pattern, P at level 9, format "▢_ n  P").
+  Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2).
+  Section S.
+  Variable n:nat.
+  Check ▢_n (n >= 1).
+  End S.
+  Fail Check ▢_nat (nat = bool).
+  Check ▢_tt (tt = tt).
+  Axiom n:nat.
+  Fail Check ▢_n (n >= 1).
+
+  End NotationMixedTermBinderAsStrictPattern.
+
+  Module AbbreviationMixedTermBinderAsStrictPattern.
+
+  Notation myforce n P := (pseudo_force n (fun n => P)).
+  Check exists x y, myforce (x,y) (x >= 1 /\ y >= 2).
+  Section S.
+  Variable n:nat.
+  Check myforce n (n >= 1). (* strict hence not used for printing *)
+  End S.
+  Fail Check myforce nat (nat = bool).
+  Check myforce tt (tt = tt).
+  Axiom n:nat.
+  Fail Check myforce n (n >= 1).
+
+  End AbbreviationMixedTermBinderAsStrictPattern.
+
+  Module Bug4765Part.
+
+  Notation id x := ((fun y => y) x).
+  Check id nat.
+
+  Notation id' x := ((fun x => x) x).
+  Check fun a : bool => id' a.
+  Check fun nat : bool => id' nat.
+  Fail Check id' nat.
+
+  End Bug4765Part.
+
+  Module NotationBinderNotMixedWithTerms.
+
+  Notation "!! x , P" := (forall x, P) (at level 200, x pattern).
+  Check !! nat, nat = true.
+
+  Notation "!!! x , P" := (forall x, P) (at level 200).
+  Check !!! nat, nat = true.
+
+  Notation "!!!! x , P" := (forall x, P) (at level 200, x strict pattern).
+  Check !!!! (nat,id), nat = true /\ id = false.
+
+  End NotationBinderNotMixedWithTerms.
+
+End P.