From cb105b62f597b2a51fad743547647e4885d6365a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Apr 2020 20:01:29 +0200
Subject: Notations: Giving a consistent role to global references occurring
 patterns.

Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.

We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.

Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
---
 interp/constrintern.ml | 195 +++++++++++++++++++++++++++++--------------------
 interp/notation_ops.ml |   2 +-
 2 files changed, 115 insertions(+), 82 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5fb6664dd6..a3dd686121 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -420,6 +420,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 +573,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 (None,env.scopes) 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 +602,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 +695,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 +722,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 +857,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 +918,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 +1609,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 =
   (* 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,7 +1633,7 @@ 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
       match Nametab.locate_extended qid with
       | SynDef sp ->
@@ -1619,39 +1641,39 @@ let drop_notations_pattern looked_for genv =
         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 +1690,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 +1704,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
       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 (terms,termlists) 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 +1747,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 +1756,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 +1785,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 +1797,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
 
 let rec intern_pat genv ntnvars aliases pat =
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
@@ -1816,19 +1838,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 scopes 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 scopes pat)
 
 let _ =
   intern_cases_pattern_fwd :=
-    fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p
+    fun test_kind ntnvars scopes p ->
+    intern_cases_pattern test_kind (Global.env ()) ntnvars scopes empty_alias p
 
 let intern_ind_pattern genv ntnvars scopes 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 scopes pat
+    with InternalizationError (NotAConstructor _) as exn ->
       let _, info = Exninfo.capture exn in
       error_bad_inductive_type ~info ()
   in
@@ -2221,7 +2254,7 @@ 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 idsl_pll = List.map (intern_cases_pattern test_kind_tolerant globalenv ntnvars (None,env.scopes) 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
@@ -2403,7 +2436,7 @@ 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
+  intern_cases_pattern test_kind_tolerant globalenv Id.Map.empty (None,[]) empty_alias patt
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 24b5dfce29..34e94d1597 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 ->
-- 
cgit v1.2.3


From 4b8a87bcebe23797c4a179dd6a1d55c058d2736f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:47:59 +0200
Subject: Passing full interning env to pattern interning, for better control.

This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
---
 interp/constrintern.ml | 36 ++++++++++++++++++++++++------------
 1 file changed, 24 insertions(+), 12 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a3dd686121..c90d789105 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)
 
@@ -575,7 +585,7 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
 
 let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
   let il,disjpat =
-    let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind 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.");
@@ -1609,7 +1619,7 @@ let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
     ~key:["Asymmetric";"Patterns"]
     ~value:false
 
-let drop_notations_pattern (test_kind_top,test_kind_inner) 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 test_kind ?loc g =
@@ -1797,7 +1807,7 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv =
       let () = assert (List.is_empty args) in
       DAst.make ?loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ?loc ()
-  in in_pat test_kind_top
+  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 =
@@ -1838,16 +1848,16 @@ 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 test_kind genv ntnvars scopes aliases pat =
+let intern_cases_pattern test_kind genv ntnvars env aliases pat =
   intern_pat genv ntnvars aliases
-    (drop_notations_pattern (test_kind,test_kind) genv scopes pat)
+    (drop_notations_pattern (test_kind,test_kind) genv env pat)
 
 let _ =
   intern_cases_pattern_fwd :=
-    fun test_kind ntnvars scopes p ->
-    intern_cases_pattern test_kind (Global.env ()) ntnvars scopes empty_alias p
+    fun test_kind ntnvars env p ->
+    intern_cases_pattern test_kind (Global.env ()) ntnvars env empty_alias p
 
-let intern_ind_pattern genv ntnvars scopes pat =
+let intern_ind_pattern genv ntnvars env pat =
   let test_kind_top ?loc = function
     | GlobRef.IndRef _  -> ()
     | GlobRef.ConstructRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ ->
@@ -1860,7 +1870,7 @@ let intern_ind_pattern genv ntnvars scopes pat =
       raise Not_found in
   let no_not =
     try
-      drop_notations_pattern (test_kind_top,test_kind_inner) genv scopes pat
+      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 ()
@@ -2254,7 +2264,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 test_kind_tolerant 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
@@ -2295,7 +2306,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")])
@@ -2436,7 +2447,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 test_kind_tolerant 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 *)
-- 
cgit v1.2.3


From c893dc56fa579c8d1f6ea3a1859681bb316d9979 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:55:15 +0200
Subject: Accept section variables in notations with mixed terms and binders.

---
 interp/notation_ops.ml | 12 +++++++++---
 pretyping/glob_ops.ml  |  1 +
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 34e94d1597..2e3fa0aa0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -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
-- 
cgit v1.2.3


From 8376231c9767d6f026ac9afc8e48c5d56cd803b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 18:06:23 +0200
Subject: Accept local variables in mixed terms and binders of notations.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c90d789105..032a752fe0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1645,6 +1645,8 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
   in
   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) =
-- 
cgit v1.2.3


From eaa25fbbd849b9c78ad6e2b16c220ae06d0b5c05 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 18:35:56 +0200
Subject: Regression tests for the various combinations of mixed terms and
 binders in notations.

This also includes tests for abbreviations.
---
 test-suite/output/Notations4.out |  54 +++++++++++++++++++++
 test-suite/output/Notations4.v   | 101 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 155 insertions(+)

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


From 7dcd829d1439a5f2d435234b72e0f595bf64eeff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:54:08 +0200
Subject: Minor cut elimination in the code of constrintern.ml.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 032a752fe0..409e46864e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1731,9 +1731,9 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
     | 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 test_kind loc scopes (terms,termlists) extrargs c
+      in_not test_kind loc scopes subst extrargs c
     | CPatDelimiters (key, e) ->
       in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e
     | CPatPrim p ->
-- 
cgit v1.2.3


From 65210210e26283f0ca247178ae7524a80d8648ff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 18:57:04 +0200
Subject: Added change log for #12099.

---
 ...ster+constraining-terms-occurring-also-as-pattern-in-notations.rst | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst

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