diff --git a/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh
new file mode 100644
index 000000000000..decb093b7187
--- /dev/null
+++ b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh
@@ -0,0 +1,3 @@
+overlay equations https://github.com/gares/Coq-Equations syndef-principal-scope 13965
+overlay elpi https://github.com/gares/coq-elpi syndef-principal-scope 13965
+overlay paramcoq https://github.com/gares/paramcoq syndef-principal-scope 13965
diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst
new file mode 100644
index 000000000000..448dbbe3c779
--- /dev/null
+++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst
@@ -0,0 +1,12 @@
+- **Added:**
+  Let the user specify a scope for abbreviation arguments, e.g.
+  ``Notation abbr X := t (X in scope my_scope)``.
+  (`#13965 <https://github.com/coq/coq/pull/13965>`_,
+  by Enrico Tassi).
+- **Changed:**
+  The error ``Argument X was previously inferred to be in scope
+  XXX_scope but is here used in YYY_scope.`` is now the warning
+  ``[inconsistent-scopes,syntax]`` and can be silenced by
+  specifying the scope of the argument
+  (`#13965 <https://github.com/coq/coq/pull/13965>`_,
+  by Enrico Tassi).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 453e878a5db3..0db9d0a86235 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1181,7 +1181,7 @@ Here are the syntax elements used by the various notation commands.
    .. prodn::
       syntax_modifier ::= at level @natural
       | in custom @ident {? at level @natural }
-      | {+, @ident } at @level
+      | {+, @ident } {| at @level | in scope @ident }
       | @ident at @level {? @binder_interp }
       | @ident @explicit_subentry
       | @ident @binder_interp
@@ -1373,6 +1373,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`.
 
    Removes the delimiting keys associated with a scope.
 
+The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted
+in a scope stack locally extended with a given scope by using the modifier
+:n:`{+, @ident } in scope @scope_name`.s
+
 Binding types or coercion classes to a notation scope
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -1566,7 +1570,7 @@ Displaying information about scopes
 Abbreviations
 --------------
 
-.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) }
+.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) }
    :name: Notation (abbreviation)
 
    .. todo: for some reason, Sphinx doesn't complain about a duplicate name if
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fd1c3c026021..b932fc6e30a5 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1410,8 +1410,9 @@ syntax_modifier: [
 | DELETE "in" "custom" IDENT
 | REPLACE "in" "custom" IDENT; "at" "level" natural
 | WITH "in" "custom" IDENT OPT ( "at" "level" natural )
-| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level
-| WITH LIST1 IDENT SEP "," "at" level
+| DELETE IDENT; "in" "scope" IDENT
+| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
+| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
 ]
 
 explicit_subentry: [
@@ -2643,7 +2644,6 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | hint
-| only_parsing
 | record_fields
 | constructor_type
 | record_binder
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ab1a9d4c750c..47c758b5e8cf 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1401,18 +1401,13 @@ syntax: [
 | "Undelimit" "Scope" IDENT
 | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
 | "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
-| "Notation" identref LIST0 ident ":=" constr only_parsing
+| "Notation" identref LIST0 ident ":=" constr syntax_modifiers
 | "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Format" "Notation" STRING STRING STRING
 | "Reserved" "Infix" ne_lstring syntax_modifiers
 | "Reserved" "Notation" ne_lstring syntax_modifiers
 ]
 
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
-]
-
 level: [
 | "level" natural
 | "next" "level"
@@ -1428,8 +1423,9 @@ syntax_modifier: [
 | "only" "printing"
 | "only" "parsing"
 | "format" STRING OPT STRING
-| IDENT; "," LIST1 IDENT SEP "," "at" level
+| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
 | IDENT; "at" level OPT binder_interp
+| IDENT; "in" "scope" IDENT
 | IDENT binder_interp
 | IDENT explicit_subentry
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 5b19b7fc5596..b0a7cb91f93a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1096,7 +1096,7 @@ command: [
 | "Undelimit" "Scope" scope_name
 | "Bind" "Scope" scope_name "with" LIST1 class
 | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
-| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
+| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
 | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Format" "Notation" string string string
 | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
@@ -1540,7 +1540,7 @@ class: [
 syntax_modifier: [
 | "at" "level" natural
 | "in" "custom" ident OPT ( "at" "level" natural )
-| LIST1 ident SEP "," "at" level
+| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ]
 | ident "at" level OPT binder_interp
 | ident explicit_subentry
 | ident binder_interp
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f02874253e4d..e72b73c36efc 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -283,10 +283,13 @@ let local_binders_loc bll = match bll with
 
 (** Folds and maps *)
 let is_constructor id =
-  try Globnames.isConstructRef
-        (Smartlocate.global_of_extended_global
-           (Nametab.locate_extended (qualid_of_ident id)))
-  with Not_found -> false
+  match
+    Smartlocate.global_of_extended_global
+      (Nametab.locate_extended (qualid_of_ident id))
+  with
+  | exception Not_found -> false
+  | None -> false
+  | Some gref -> Globnames.isConstructRef gref
 
 let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
   | CPatRecord l ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 958e1408f88f..68dd96e44be1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -273,40 +273,54 @@ let make_current_scope tmp scopes = match tmp, scopes with
   | Some tmp_scope, scopes -> tmp_scope :: scopes
   | None, scopes -> scopes
 
-let pr_scope_stack = function
-  | [] -> str "the empty scope stack"
-  | [a] -> str "scope " ++ str a
-  | l -> str "scope stack " ++
+let pr_scope_stack begin_of_sentence l =
+  let bstr x =
+    if begin_of_sentence then str (CString.capitalize_ascii x) else str x in
+  match l with
+  | [] -> bstr "the empty scope stack"
+  | [a] -> bstr "scope " ++ str a
+  | l -> bstr "scope stack " ++
       str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
 
-let error_inconsistent_scope ?loc id scopes1 scopes2 =
-  user_err ?loc ~hdr:"set_var_scope"
-   (Id.print id ++ str " is here used in " ++
-    pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
-    pr_scope_stack scopes1)
+let warn_inconsistent_scope =
+  CWarnings.create ~name:"inconsistent-scopes" ~category:"syntax"
+    (fun (id,scopes1,scopes2) ->
+      (str "Argument " ++ Id.print id ++
+       strbrk " was previously inferred to be in " ++
+       pr_scope_stack false scopes1 ++
+       strbrk " but is here used in " ++
+       pr_scope_stack false scopes2 ++
+       strbrk ". " ++
+       pr_scope_stack true scopes1 ++
+       strbrk " will be used at parsing time unless you override it by" ++
+       strbrk " annotating the argument with an explicit scope of choice."))
 
 let error_expect_binder_notation_type ?loc id =
   user_err ?loc
    (Id.print id ++
     str " is expected to occur in binding position in the right-hand side.")
 
-let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
+let set_notation_var_scope ?loc id (tmp_scope,subscopes as scopes) ntnvars =
   try
-    let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
-    if istermvar then begin
-      (* scopes have no effect on the interpretation of identifiers *)
-      (match !idscopes with
+    let _,idscopes,typ = Id.Map.find id ntnvars in
+    match typ with
+    | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
+    | Notation_term.NtnInternTypeAny principal ->
+      match !idscopes with
       | None -> idscopes := Some scopes
       | Some (tmp_scope', subscopes') ->
         let s' = make_current_scope tmp_scope' subscopes' in
         let s = make_current_scope tmp_scope subscopes in
-        if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s);
-      (match typ with
-      | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
-      | Notation_term.NtnInternTypeAny -> ())
-      end
-    else
-      used_as_binder := true
+        if Option.is_empty principal && not (List.equal String.equal s' s) then
+          warn_inconsistent_scope ?loc (id,s',s)
+ with Not_found ->
+    (* Not in a notation *)
+    ()
+
+let set_var_is_binder ?loc id ntnvars =
+  try
+    let used_as_binder,_,_ = Id.Map.find id ntnvars in
+    used_as_binder := true
   with Not_found ->
     (* Not in a notation *)
     ()
@@ -484,7 +498,7 @@ let push_name_env ntnvars implargs env =
   | { loc; v = Name id } ->
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
-      set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
+      set_var_is_binder ?loc id ntnvars;
       let uid = var_uid id in
       Dumpglob.dump_binding ?loc uid;
       pure_push_name_env (id,(Variable,implargs,[],uid)) env
@@ -1064,7 +1078,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] a notation variable *)
   if Id.Map.mem id ntnvars then
     begin
-      if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars;
+      if not (Id.Map.mem id env.impls) then set_notation_var_scope ?loc id (env.tmp_scope,env.scopes) ntnvars;
       gvar (loc,id) us
     end
   else
@@ -1130,14 +1144,54 @@ let intern_reference qid =
   in
   Smartlocate.global_of_extended_global r
 
+let intern_sort_name ~local_univs = function
+  | CSProp -> GSProp
+  | CProp -> GProp
+  | CSet -> GSet
+  | CRawType u -> GRawUniv u
+  | CType qid ->
+    let is_id = qualid_is_ident qid in
+    let local = if not is_id then None
+      else Id.Map.find_opt (qualid_basename qid) local_univs.bound
+    in
+    match local with
+    | Some u -> GUniv u
+    | None ->
+      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
+      with Not_found ->
+        if is_id && local_univs.unb_univs
+        then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
+        else
+          CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
+
+let intern_sort ~local_univs s =
+  map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
+
+let intern_instance ~local_univs us =
+  Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
+
+let intern_name_alias = function
+  | { CAst.v = CRef(qid,u) } ->
+      let r =
+        try Some (intern_extended_global_of_qualid qid)
+        with Not_found -> None
+      in
+      Option.bind r Smartlocate.global_of_extended_global |>
+      Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u)
+  | _ -> None
+
 let intern_projection qid =
-  try
-    match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with
-    | GlobRef.ConstRef c as gr ->
-        (gr, Structure.find_from_projection c)
-    | _ -> raise Not_found
-  with Not_found ->
-    Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  match
+    Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |>
+    Option.map (function
+     | GlobRef.ConstRef c as x -> x, Structure.find_from_projection c
+     | _ -> raise Not_found)
+  with
+  | exception Not_found ->
+     Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  | None ->
+     Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  | Some x -> x
 
 (**********************************************************************)
 (* Interpreting references                                            *)
@@ -1182,37 +1236,6 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
   | UAnonymous {rigid} -> UAnonymous {rigid}
   | UNamed id -> UNamed [id,0]
 
-let intern_sort_name ~local_univs = function
-  | CSProp -> GSProp
-  | CProp -> GProp
-  | CSet -> GSet
-  | CRawType u -> GRawUniv u
-  | CType qid ->
-    let is_id = qualid_is_ident qid in
-    let local = if not is_id then None
-      else Id.Map.find_opt (qualid_basename qid) local_univs.bound
-    in
-    match local with
-    | Some u -> GUniv u
-    | None ->
-      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
-      with Not_found ->
-        if is_id && local_univs.unb_univs
-        then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
-        else
-          CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
-
-let intern_sort ~local_univs s =
-  map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
-
-let intern_instance ~local_univs us =
-  Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
-
-let try_interp_name_alias = function
-  | [], { CAst.v = CRef (ref,u) } ->
-     NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u)
-  | _ -> raise Not_found
-
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   let loc = qid.loc in
@@ -1843,7 +1866,7 @@ let rec intern_pat genv ntnvars aliases pat =
       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;
+      set_var_is_binder ?loc id ntnvars;
       (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *)
     | RCPatAtom None ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
@@ -2561,7 +2584,11 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   let ids = extract_ids env in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
+  let vl = Id.Map.map (function
+    | (NtnInternTypeAny None | NtnInternTypeOnlyBinder) as typ -> (ref false, ref None, typ)
+    | NtnInternTypeAny (Some scope) as typ ->
+        (ref false, ref (Some (Some scope,[])), typ)
+    ) nenv.ninterp_var_type in
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize env
       {ids; unb = false;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 65b63962d065..379bd610706c 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -147,12 +147,13 @@ val interp_constr_pattern :
   env -> evar_map -> ?expected_type:typing_constraint ->
     constr_pattern_expr -> constr_pattern
 
-(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : qualid -> GlobRef.t
+(** Returns None if it's a syndef not bound to a name, raises an error
+    if not existing *)
+val intern_reference : qualid -> GlobRef.t option
 
-(** For syntactic definitions: check if abbreviation to a name
-    and avoid early insertion of maximal implicit arguments *)
-val try_interp_name_alias : 'a list * constr_expr -> notation_constr
+(** Returns None if not a reference or a syndef not bound to a name *)
+val intern_name_alias :
+  constr_expr -> (GlobRef.t * Glob_term.glob_level list option) option
 
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> qualid -> glob_constr
@@ -174,7 +175,7 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition
    (these functions do not modify the glob file) *)
 
-val locate_reference :  Libnames.qualid -> GlobRef.t
+val locate_reference :  Libnames.qualid -> GlobRef.t option
 val is_global : Id.t -> bool
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ea5e2a1ad4fa..ced102c703e2 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -681,7 +681,7 @@ let check_variables_and_reversibility nenv
         str " position as part of a recursive pattern.") in
   let check_type x typ =
     match typ with
-    | NtnInternTypeAny ->
+    | NtnInternTypeAny _ ->
         begin
           try check_pair "term" x (Id.Map.find x recvars) foundrec
           with Not_found -> check_bound x
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 2979447cf83c..ec7165f854dc 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -91,7 +91,8 @@ type notation_var_instance_type =
     in a recursive pattern x..y, both x and y carry the individual type
     of each element of the list x..y *)
 type notation_var_internalization_type =
-  | NtnInternTypeAny | NtnInternTypeOnlyBinder
+  | NtnInternTypeAny of scope_name option
+  | NtnInternTypeOnlyBinder
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 91d05f7317da..56b3cd98155b 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -33,7 +33,7 @@ let global_of_extended_global_head = function
         | _ -> raise Not_found in
       head_of syn_def
 
-let global_of_extended_global = function
+let global_of_extended_global_exn = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
   match search_syntactic_definition kn with
@@ -45,11 +45,15 @@ let locate_global_with_alias ?(head=false) qid =
   let ref = Nametab.locate_extended qid in
   try
     if head then global_of_extended_global_head ref
-    else global_of_extended_global ref
+    else global_of_extended_global_exn ref
   with Not_found ->
     user_err ?loc:qid.CAst.loc (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
+let global_of_extended_global x =
+  try Some (global_of_extended_global_exn x)
+  with Not_found -> None
+
 let global_constant_with_alias qid  =
   try match locate_global_with_alias qid with
   | Names.GlobRef.ConstRef c -> c
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 26f2a4f36d43..abf9839c9e3b 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -19,8 +19,9 @@ open Globnames
 
 val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
-(** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> GlobRef.t
+(** Extract a global_reference from a reference that can be an "alias".
+    If the reference points to a more complex term, we return None *)
+val global_of_extended_global : extended_global_reference -> GlobRef.t option
 
 (** Locate a reference taking into account possible "alias" notations.
     May raise [Nametab.GlobalizationError _] for an unknown reference,
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3234d40f7315..7d19c443e9d8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
           (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
           let evd', res =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference
-                 (qualid_of_ident equation_lemma_id))
+              (Option.get (Constrintern.locate_reference
+                 (qualid_of_ident equation_lemma_id)))
           in
           evd := evd';
           let sigma, _ =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc86..598044650828 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -241,7 +241,7 @@ let change_property_sort evd toSort princ princName =
   in
   let evd, princName_as_constr =
     Evd.fresh_global (Global.env ()) evd
-      (Constrintern.locate_reference (Libnames.qualid_of_ident princName))
+      (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident princName)))
   in
   let init =
     let nargs =
@@ -408,8 +408,8 @@ let register_struct is_rec fixpoint_exprl =
         (fun (evd, l) {Vernacexpr.fname} ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference
-                 (Libnames.qualid_of_ident fname.CAst.v))
+              (Option.get (Constrintern.locate_reference
+                 (Libnames.qualid_of_ident fname.CAst.v)))
           in
           let cst, u = destConst evd c in
           let u = EInstance.kind evd u in
@@ -427,8 +427,8 @@ let register_struct is_rec fixpoint_exprl =
         (fun (evd, l) {Vernacexpr.fname} ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference
-                 (Libnames.qualid_of_ident fname.CAst.v))
+              (Option.get (Constrintern.locate_reference
+                 (Libnames.qualid_of_ident fname.CAst.v)))
           in
           let cst, u = destConst evd c in
           let u = EInstance.kind evd u in
@@ -1522,7 +1522,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
           let _, lem_cst_constr =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
           in
           let lem_cst, _ = EConstr.destConst !evd lem_cst_constr in
           update_Function {finfo with correctness_lemma = Some lem_cst})
@@ -1592,7 +1592,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           in
           let _, lem_cst_constr =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
           in
           let lem_cst, _ = destConst !evd lem_cst_constr in
           update_Function {finfo with completeness_lemma = Some lem_cst})
@@ -1615,7 +1615,7 @@ let derive_inversion fix_names =
         (fun id (evd, l) ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id)))
           in
           let cst, u = EConstr.destConst evd c in
           (evd, (cst, EConstr.EInstance.kind evd u) :: l))
@@ -1635,8 +1635,8 @@ let derive_inversion fix_names =
           (fun id (evd, l) ->
             let evd, id =
               Evd.fresh_global (Global.env ()) evd
-                (Constrintern.locate_reference
-                   (Libnames.qualid_of_ident (mk_rel_id id)))
+                (Option.get (Constrintern.locate_reference
+                   (Libnames.qualid_of_ident (mk_rel_id id))))
             in
             (evd, fst (EConstr.destInd evd id) :: l))
           fix_names (evd', [])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4e0e2dc501fb..1221ad0bda91 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat =
                   (elimination_sort_of_goal gl)
               in
               let princ_ref =
-                try
+                match
                   Constrintern.locate_reference
                     (Libnames.qualid_of_ident princ_name)
-                with Not_found ->
+                with
+                | Some r -> r
+                | None ->
                   user_err
                     ( str "Cannot find induction principle for "
                     ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v
index 6ff394bca64d..8d7d97d7aa0f 100644
--- a/test-suite/bugs/closed/bug_3468.v
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
 Definition test := (& (@4))%my.
 
 (* Check inconsistent scopes *)
+Set Warnings "+inconsistent-scopes".
 Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).
diff --git a/test-suite/output/notation_principal_scope.out b/test-suite/output/notation_principal_scope.out
new file mode 100644
index 000000000000..5ccee259b0c0
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+Argument X was previously inferred to be in scope function_scope but is here
+used in the empty scope stack. Scope function_scope will be used at parsing
+time unless you override it by annotating the argument with an explicit scope
+of choice. [inconsistent-scopes,syntax]
+The command has indeed failed with message:
+Simple notations don't support only printing
+The command has indeed failed with message:
+The reference nonexisting was not found in the current environment.
+The command has indeed failed with message:
+Notation scope for argument X can be specified only once.
+pp I
+     : True /\ True
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "I" of type "True" cannot be applied to the term
+ "I" : "True"
+File "stdin", line 21, characters 0-50:
+Warning: This notation will not be used for printing as it is bound to a
+single variable. [notation-bound-to-variable,parsing]
diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v
new file mode 100644
index 000000000000..6bd911501d87
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.v
@@ -0,0 +1,23 @@
+Arguments conj {_ _} _ _%function.
+
+Set Warnings "+inconsistent-scopes".
+Fail Notation pp X := (conj X X).
+
+Fail Notation pp := 1 (only printing).
+
+Fail Notation pp X := nonexisting.
+
+Fail Notation pp X := (conj X X) (X, X in scope nat_scope).
+
+Notation pp X := (conj X X) (X in scope nat_scope).
+
+Notation "$" := I (only parsing) : nat_scope.
+Notation "$" := (I I) (only parsing) : bool_scope.
+
+Open Scope bool_scope.
+Check pp $.
+Fail Check pp (id $).
+
+Notation pp1 X := (X%nat) (X in scope bool_scope).
+Notation pp2 X := ((X + X)%type) (X in scope bool_scope).
+Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope).
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f8a28332b137..2343ffc7e748 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -52,7 +52,6 @@ let of_type = Entry.create "of_type"
 let section_subset_expr = Entry.create "section_subset_expr"
 let scope_delimiter = Entry.create "scope_delimiter"
 let syntax_modifiers = Entry.create "syntax_modifiers"
-let only_parsing = Entry.create "only_parsing"
 
 let make_bullet s =
   let open Proof_bullet in
@@ -1160,7 +1159,7 @@ GRAMMAR EXTEND Gram
 (* Grammar extensions *)
 
 GRAMMAR EXTEND Gram
-  GLOBAL: syntax only_parsing syntax_modifiers;
+  GLOBAL: syntax syntax_modifiers;
 
   syntax:
    [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
@@ -1181,10 +1180,9 @@ GRAMMAR EXTEND Gram
          modl = syntax_modifiers;
          sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
          { VernacInfix ((op,modl),p,sc) }
-     | IDENT "Notation"; id = identref;
-         idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
-           { VernacSyntacticDefinition
-             (id,(idl,c),{ onlyparsing = b }) }
+     | IDENT "Notation"; id = identref; idl = LIST0 ident;
+         ":="; c = constr; modl = syntax_modifiers ->
+           { VernacSyntacticDefinition (id,(idl,c), modl) }
      | IDENT "Notation"; s = lstring; ":=";
          c = constr;
          modl = syntax_modifiers;
@@ -1207,10 +1205,6 @@ GRAMMAR EXTEND Gram
         to factorize with other "Print"-based or "Declare"-based vernac entries *)
   ] ]
   ;
-  only_parsing:
-    [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true }
-      | -> { false } ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> { NumLevel n }
       | IDENT "next"; IDENT "level" -> { NextLevel } ] ]
@@ -1230,10 +1224,12 @@ GRAMMAR EXTEND Gram
           { begin match s1, s2 with
           | { CAst.v = k }, Some s -> SetFormat(k,s)
           | s, None -> SetFormat ("text",s) end }
-      | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
-        lev = level -> { SetItemLevel (x::l,None,lev) }
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; v =
+          [ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) }
+          | "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l }
       | x = IDENT; "at"; lev = level; b = OPT binder_interp ->
         { SetItemLevel ([x],b,lev) }
+      | x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) }
       | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
       | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
     ] ]
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f9f65a8c30d9..c5bfba900c8a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -862,6 +862,41 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
 (* Interpreting user-provided modifiers *)
 
 (* XXX: We could move this to the parser itself *)
+
+module SyndefMods = struct
+
+type t = {
+  only_parsing  : bool;
+  scopes : (Id.t * scope_name) list;
+}
+
+let default = {
+  only_parsing  = false;
+  scopes = [];
+}
+
+end
+
+let interp_syndef_modifiers modl = let open SyndefMods in
+  let rec interp skipped acc = function
+    | [] -> List.rev skipped, acc
+    | SetOnlyParsing :: l ->
+        interp skipped { acc with only_parsing = true; } l
+    | SetItemScope([],_) :: l ->
+        interp skipped acc l
+    | SetItemScope(s::ids,k) :: l ->
+        let scopes = acc.scopes in
+        let id = Id.of_string s in
+        if List.mem_assoc id scopes then
+          user_err (str "Notation scope for argument " ++ str s ++
+                    str " can be specified only once.");
+        interp skipped { acc with scopes = (id,k) :: scopes }
+          (SetItemScope(ids,s) :: l)
+    | x :: l ->
+        interp (x :: skipped) acc l
+ in
+   interp [] default modl
+
 module NotationMods = struct
 
 type notation_modifier = {
@@ -872,7 +907,6 @@ type notation_modifier = {
   subtyps       : (Id.t * production_level) list;
 
   (* common to syn_data below *)
-  only_parsing  : bool;
   only_printing : bool;
   format        : lstring option;
   extra         : (string * string) list;
@@ -884,7 +918,6 @@ let default = {
   custom        = InConstrEntry;
   etyps         = [];
   subtyps       = [];
-  only_parsing  = false;
   only_printing = false;
   format        = None;
   extra         = [];
@@ -945,8 +978,6 @@ let interp_modifiers modl = let open NotationMods in
     | SetAssoc a :: l ->
         if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
         interp subtyps { acc with assoc = Some a; } l
-     | SetOnlyParsing :: l ->
-        interp subtyps { acc with only_parsing = true; } l
     | SetOnlyPrinting :: l ->
         interp subtyps { acc with only_printing = true; } l
     | SetFormat ("text",s) :: l ->
@@ -954,8 +985,10 @@ let interp_modifiers modl = let open NotationMods in
         interp subtyps { acc with format = Some s; } l
     | SetFormat (k,s) :: l ->
         interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
+    | (SetOnlyParsing | SetItemScope _) :: _ -> assert false
   in
-  let subtyps,mods = interp [] default modl in
+  let modl, syndef_mods = interp_syndef_modifiers modl in
+  let subtyps, mods = interp [] default modl in
   (* interpret item levels wrt to main entry *)
   let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in
   (* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *)
@@ -965,10 +998,10 @@ let interp_modifiers modl = let open NotationMods in
            if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true))
            else (id,ETIdent)
         | x -> x) mods.etyps } in
-  { mods with etyps = extra_etyps@mods.etyps }
+  syndef_mods, { mods with etyps = extra_etyps@mods.etyps }
 
 let check_infix_modifiers modifiers =
-  let mods = interp_modifiers modifiers in
+  let _, mods = interp_modifiers modifiers in
   let t = mods.NotationMods.etyps in
   let u = mods.NotationMods.subtyps in
   if not (List.is_empty t) || not (List.is_empty u) then
@@ -1036,7 +1069,7 @@ let join_auxiliary_recursive_types recvars etyps =
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
   | ETConstr _ | ETBigint | ETGlobal
-  | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny
+  | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny None
 
 let set_internalization_type typs =
   List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -1292,23 +1325,25 @@ let check_locality_compatibility local custom i_typs =
 
 let compute_syntax_data ~local deprecation df modifiers =
   let open SynData in
+  let open SyndefMods in
   let open NotationMods in
-  let mods = interp_modifiers modifiers in
-  let onlyprint = mods.only_printing in
-  let onlyparse = mods.only_parsing in
-  if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
+  let syndef_mods, mods = interp_modifiers modifiers in
+  let only_printing = mods.only_printing in
+  let only_parsing = syndef_mods.only_parsing in
+  if only_printing && only_parsing then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
+  if syndef_mods.scopes <> [] then user_err (str "General notations don't support 'in scope'.");
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
-  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint:only_printing df in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
 
   (* Notations for interp and grammar  *)
-  let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
+  let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols only_printing in
   let ntn_for_interp = make_notation_key mods.custom symbols in
   let symbols_for_grammar =
     if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
   let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in
-  if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
+  if mods.custom = InConstrEntry && not only_printing then check_rule_productivity symbols_for_grammar;
   (* To globalize... *)
   let etyps = join_auxiliary_recursive_types recvars mods.etyps in
   let sy_typs, prec =
@@ -1329,8 +1364,8 @@ let compute_syntax_data ~local deprecation df modifiers =
   (* Return relevant data for interpretation and for parsing/printing *)
   { info = i_data;
 
-    only_parsing  = mods.only_parsing;
-    only_printing = mods.only_printing;
+    only_parsing;
+    only_printing;
     deprecation;
     format        = mods.format;
     extra         = mods.extra;
@@ -1793,11 +1828,18 @@ let remove_delimiters local scope =
 let add_class_scope local scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
 
-let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
+let add_syntactic_definition ~local deprecation env ident (vars,c) modl =
+  let open SyndefMods in
+  let skipped, { only_parsing; scopes } = interp_syndef_modifiers modl in
+  if skipped <> [] then
+    user_err (str "Simple notations don't support " ++ Ppvernac.pr_syntax_modifier (List.hd skipped));
+  let vars = List.map (fun v -> v, List.assoc_opt v scopes) vars in
   let acvars,pat,reversibility =
-    try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
-    with Not_found ->
-      let fold accu id = Id.Map.add id NtnInternTypeAny accu in
+    match vars, intern_name_alias c with
+    | [], Some(r,u) ->
+      Id.Map.empty, NRef(r, u), APrioriReversible
+    | _ ->
+      let fold accu (id,scope) = Id.Map.add id (NtnInternTypeAny scope) accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
       let nenv = {
         ninterp_var_type = i_vars;
@@ -1805,11 +1847,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
       } in
       interp_notation_constr env nenv c
   in
-  let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
+  let in_pat (id,_) = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
   let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in
-  let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
+  let vars = List.map (fun (x,_) -> (x, Id.Map.find x interp)) vars in
   let also_in_cases_pattern = has_no_binders_type vars in
-  let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
+  let onlyparsing = only_parsing || fst (printability None [] false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat)
 
 (**********************************************************************)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index dd71817083d3..3ece04f5f98a 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
-  Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit
+  Id.t -> Id.t list * constr_expr -> syntax_modifier list -> unit
 
 (** Print the Camlp5 state of a grammar *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 8e5942440b50..be34c563c809 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -468,6 +468,8 @@ let pr_syntax_modifier = let open Gramlib.Gramext in function
     | SetItemLevel (l,bko,n) ->
       prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
       pr_opt pr_constr_as_binder_kind bko
+    | SetItemScope (l,s) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ str"in scope" ++ str s
     | SetLevel n -> pr_at_level (NumLevel n)
     | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
     | SetAssoc LeftA -> keyword "left associativity"
@@ -484,9 +486,6 @@ let pr_syntax_modifiers = function
   | l -> spc() ++
          hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-let pr_only_parsing_clause onlyparsing =
-  pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
-
 let pr_decl_notation prc decl_ntn =
   let open Vernacexpr in
   let
@@ -1098,12 +1097,12 @@ let pr_vernac_expr v =
     )
   | VernacHints (dbnames,h) ->
     return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
-  | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
+  | VernacSyntacticDefinition (id,(ids,c),l) ->
     return (
       hov 2
         (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
          prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
-         pr_only_parsing_clause onlyparsing)
+         pr_syntax_modifiers l)
     )
   | VernacArguments (q, args, more_implicits, mods) ->
     return (
diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli
index 933980394813..d36e61864d69 100644
--- a/vernac/ppvernac.mli
+++ b/vernac/ppvernac.mli
@@ -13,6 +13,8 @@
 
 val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 
+val pr_syntax_modifier : Vernacexpr.syntax_modifier -> Pp.t
+
 (** Prints a fixpoint body *)
 val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 46acaf7264a6..9757783d096b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -114,10 +114,6 @@ type import_filter_expr =
   | ImportAll
   | ImportNames of one_import_filter_name list
 
-type onlyparsing_flag = { onlyparsing : bool }
- (* Some v = Parse only;  None = Print also.
-    If v<>Current, it contains the name of the coq version
-    which this notation is trying to be compatible with *)
 type locality_flag  = bool (* true = Local *)
 
 type option_setting =
@@ -135,6 +131,7 @@ type definition_expr =
 
 type syntax_modifier =
   | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
+  | SetItemScope of string list * scope_name
   | SetLevel of int
   | SetCustomEntry of string * int option
   | SetAssoc of Gramlib.Gramext.g_assoc
@@ -411,8 +408,7 @@ type nonrec vernac_expr =
   | VernacRemoveHints of string list * qualid list
   | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of
-      lident * (Id.t list * constr_expr) *
-      onlyparsing_flag
+      lident * (Id.t list * constr_expr) * syntax_modifier list
   | VernacArguments of
       qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *