Adding support for custom entries in notations.

- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
  entries. This typically corresponds to rules of the form
  'Notation "[ x ]" := x (x custom myconstr).' but also
  'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
  are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
  are natively recognized.

Incidentally merging ETConstr and ETConstrAsBinder.

Noticed in passing that parsing binder as custom was not done as in
constr.

Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.

38 files changed, 920 insertions, 436 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 521eeb8e96..d8dd4ef6dd 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -20,7 +20,10 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
-type notation = string
+type notation_entry = InConstrEntry | InCustomEntry of string
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_key = string
+type notation = notation_entry_level * notation_key
 
 type 'a or_by_notation_r =
   | AN of 'a
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4b1af9147c..011c4a6e4e 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -16,6 +16,7 @@ open Libnames
 open Namegen
 open Glob_term
 open Constrexpr
+open Notation
 open Decl_kinds
 
 (***********************)
@@ -80,7 +81,7 @@ let rec cases_pattern_expr_eq p1 p2 =
   | CPatOr a1, CPatOr a2 ->
     List.equal cases_pattern_expr_eq a1 a2
   | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
-    String.equal n1 n2 &&
+    notation_eq n1 n2 &&
     cases_pattern_notation_substitution_eq s1 s2 &&
     List.equal cases_pattern_expr_eq l1 l2
   | CPatPrim i1, CPatPrim i2 ->
@@ -165,7 +166,7 @@ let rec constr_expr_eq e1 e2 =
   | CCast(t1,c1), CCast(t2,c2) ->
     constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(n1, s1), CNotation(n2, s2) ->
-      String.equal n1 n2 &&
+      notation_eq n1 n2 &&
       constr_notation_substitution_eq s1 s2
     | CPrim i1, CPrim i2 ->
       prim_token_eq i1 i2
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 46aef1c788..61e8aa1b51 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -107,8 +107,8 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
 
 val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
 
-val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
-val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
+val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
+val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list
 
 (** For cases pattern parsing errors *)
 val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2538c77722..009894fddb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -101,7 +101,7 @@ let _show_inactive_notations () =
     IRuleSet.iter
       (function
        | NotationRule (scopt, ntn) ->
-         Feedback.msg_notice (str ntn ++ show_scope scopt)
+         Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
        | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
       !inactive_notations_table
 
@@ -113,14 +113,14 @@ let deactivate_notation nr =
   | NotationRule (scopt, ntn) ->
      match availability_of_notation (scopt, ntn) (scopt, []) with
      | None -> user_err ~hdr:"Notation"
-                        (str ntn ++ spc () ++ str "does not exist"
+                        (pr_notation ntn ++ spc () ++ str "does not exist"
                          ++ (match scopt with
                              | None -> spc () ++ str "in the empty scope."
                              | Some _ -> show_scope scopt ++ str "."))
      | Some _ ->
         if IRuleSet.mem nr !inactive_notations_table then
           Feedback.msg_warning
-            (str "Notation" ++ spc () ++ str ntn ++ spc ()
+            (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
              ++ str "is already inactive" ++ show_scope scopt ++ str ".")
         else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
 
@@ -131,7 +131,7 @@ let reactivate_notation nr =
   with Not_found ->
     match nr with
     | NotationRule (scopt, ntn) ->
-       Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc ()
+       Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
                              ++ str "is already active" ++ show_scope scopt ++
   str ".")
     | SynDefRule kn ->
@@ -260,6 +260,14 @@ let insert_pat_alias ?loc p = function
   | Anonymous -> p
   | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
 
+let rec insert_coercion ?loc l c = match l with
+  | [] -> c
+  | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+
+let rec insert_pat_coercion ?loc l c = match l with
+  | [] -> c
+  | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
+
 (**********************************************************************)
 (* conversion of references                                           *)
 
@@ -325,16 +333,16 @@ let is_zero s =
   in aux 0
 
 let make_notation_gen loc ntn mknot mkprim destprim l bl =
-  match ntn,List.map destprim l with
+  match snd ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         assert (bl=[]);
-        mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[])
+        mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], [] when is_number x ->
+        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
 	   mkprim (loc, Numeral (x,false))
-	| [Terminal x], [] when is_number x ->
+        | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
 	   mkprim (loc, Numeral (x,true))
         | _ -> mknot (loc,ntn,l,bl)
 
@@ -367,31 +375,39 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
-let lift f c =
-  let loc = c.CAst.loc in
-  CAst.make ?loc (f ?loc (DAst.get c))
-
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
+let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
     if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+      | None -> raise No_match
+      | Some coercion ->
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
       | Some key ->
 	let loc = cases_pattern_loc pat in
-	insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
+        insert_pat_coercion ?loc coercion
+          (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
   with No_match ->
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_notation_pattern scopes vars pat
+      extern_notation_pattern allscopes vars pat
         (uninterp_cases_pattern_notations pat)
     with No_match ->
-      lift (fun ?loc -> function
-        | PatVar (Name id) -> CPatAtom (Some (qualid_of_ident ?loc id))
-	| PatVar (Anonymous) -> CPatAtom None
+    let loc = pat.CAst.loc in
+    match DAst.get pat with
+    | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+    | pat ->
+    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+    | None -> raise No_match
+    | Some coercion ->
+      let allscopes = (InConstrEntrySomeLevel,scopes) in
+      let pat = match pat with
+        | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+        | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
 	| PatCstr(cstrsp,args,na) ->
-	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+          let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
 	  let p =
 	    try
               if !Flags.raw_print then raise Exit;
@@ -424,26 +440,32 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
 		      | Some true_args -> CPatCstr (c, None, true_args)
 		      | None           -> CPatCstr (c, Some full_args, [])
-	  in (insert_pat_alias ?loc (CAst.make ?loc p) na).v
-        ) pat
+          in
+          insert_pat_alias ?loc (CAst.make ?loc p) na
+      in
+      insert_pat_coercion coercion pat
+
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
-    (tmp_scope, scopes as allscopes) vars =
+    (custom, (tmp_scope, scopes) as allscopes) vars =
   function
     | NotationRule (sc,ntn) ->
       begin
-	match availability_of_notation (sc,ntn) allscopes with
+        match availability_of_entry_coercion custom (fst ntn) with
+        | None -> raise No_match
+        | Some coercion ->
+        match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
 	  (* Uninterpretation is not allowed in current context *)
 	  | None -> raise No_match
 	  (* Uninterpretation is allowed in current context *)
 	  | Some (scopt,key) ->
 	    let scopes' = Option.List.cons scopt scopes in
 	    let l =
-	      List.map (fun (c,(scopt,scl)) ->
-		extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
+              List.map (fun (c,(subentry,(scopt,scl))) ->
+                extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
 		subst in
 	    let ll =
-	      List.map (fun (c,(scopt,scl)) ->
-		let subscope = (scopt,scl@scopes') in
+              List.map (fun (c,(subentry,(scopt,scl))) ->
+                let subscope = (subentry,(scopt,scl@scopes')) in
 		List.map (extern_cases_pattern_in_scope subscope vars) c)
 		substlist in
 	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
@@ -453,14 +475,15 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
 		  |Some true_args -> true_args
 		  |None -> raise No_match
 	    in
-	    insert_pat_delimiters ?loc
-	      (make_pat_notation ?loc ntn (l,ll) l2') key
+            insert_pat_coercion coercion
+              (insert_pat_delimiters ?loc
+                 (make_pat_notation ?loc ntn (l,ll) l2') key)
       end
     | SynDefRule kn ->
       let qid = shortest_qualid_of_syndef ?loc vars kn in
       let l1 =
-	List.rev_map (fun (c,(scopt,scl)) ->
-          extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
+        List.rev_map (fun (c,(subentry,(scopt,scl))) ->
+          extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
       let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
       let l2' = if !asymmetric_patterns then l2
@@ -471,7 +494,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       in
       assert (List.is_empty substlist);
       mkPat ?loc qid (List.rev_append l1 l2')
-and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation_pattern allscopes vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
@@ -498,35 +521,38 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
     with
 	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
 
-let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
+let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
     let c = extern_reference vars (IndRef ind) in
-    let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+    let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
       let (sc,p) = uninterp_prim_token_ind_pattern ind args in
+      match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+        | None -> raise No_match
+        | Some coercion ->
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
 	| Some key ->
-	  insert_pat_delimiters (CAst.make @@ CPatPrim p) key
+          insert_pat_coercion coercion (insert_pat_delimiters (CAst.make @@ CPatPrim p) key)
     with No_match ->
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
-	extern_notation_ind_pattern scopes vars ind args
+        extern_notation_ind_pattern allscopes vars ind args
           (uninterp_ind_pattern_notations ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
-      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+      let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
 	   |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
 	   |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
-  extern_cases_pattern_in_scope (None,[]) vars p
+  extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -640,12 +666,12 @@ let extern_app inctx impl (cf,f) us args =
   else
     explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
 
-let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
 | [], _ -> []
 | a :: args, scopt :: subscopes ->
-  (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes
+  (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
 | a :: args, [] ->
-  (a, (None, scopes)) :: fill_arg_scopes args [] scopes
+  (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -697,12 +723,15 @@ let rec flatten_application c = match DAst.get c with
 (* mapping glob_constr to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
 
-let extern_possible_prim_token scopes r =
+let extern_possible_prim_token (custom,scopes) r =
   try
     let (sc,n) = uninterp_prim_token r in
+    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+    | None -> raise No_match
+    | Some coercion ->
     match availability_of_prim_token n sc scopes with
     | None -> None
-    | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+    | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key))
   with No_match ->
     None
 
@@ -737,7 +766,13 @@ let extern_glob_sort = function
 let extern_universes = function
   | Some _ as l when !print_universes -> l
   | _ -> None
-  
+
+let extern_ref vars ref us =
+  extern_global (select_stronger_impargs (implicits_of_global ref))
+    (extern_reference vars ref) (extern_universes us)
+
+let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
+
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try
@@ -748,12 +783,27 @@ let rec extern inctx scopes vars r =
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_notation scopes vars r'' (uninterp_notations r'')
-  with No_match -> lift (fun ?loc -> function
-  | GRef (ref,us) ->
-      extern_global (select_stronger_impargs (implicits_of_global ref))
-        (extern_reference vars ref) (extern_universes us)
+  with No_match ->
+  let loc = r'.CAst.loc in
+  match DAst.get r' with
+  | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
+
+  | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+
+  | c ->
+
+  match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+  | None -> raise No_match
+  | Some coercion ->
 
-  | GVar id -> CRef (qualid_of_ident ?loc id,None)
+  let scopes = (InConstrEntrySomeLevel, snd scopes) in
+  let c = match c with
+
+  (* The remaining cases are only for the constr entry *)
+
+  | GRef (ref,us) -> extern_ref vars ref us
+
+  | GVar id -> extern_var ?loc id
 
   | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
 
@@ -770,7 +820,7 @@ let rec extern inctx scopes vars r =
       (match DAst.get f with
 	 | GRef (ref,us) ->
 	     let subscopes = find_arguments_scope ref in
-	     let args = fill_arg_scopes args subscopes (snd scopes) in
+             let args = fill_arg_scopes args subscopes scopes in
 	     begin
 	       try
                  if !Flags.raw_print then raise Exit;
@@ -921,12 +971,13 @@ let rec extern inctx scopes vars r =
   | GProj (p, c) ->
     let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
     CProj (pr, sub_extern inctx scopes vars c)
-  ) r'
 
-and extern_typ (_,scopes) =
-  extern true (Notation.current_type_scope_name (),scopes)
+  in insert_coercion coercion (CAst.make ?loc c)
+
+and extern_typ (subentry,(_,scopes)) =
+  extern true (subentry,(Notation.current_type_scope_name (),scopes))
 
-and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
+and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
 
 and factorize_prod scopes vars na bk aty c =
   let store, get = set_temporary_memory () in
@@ -1019,7 +1070,7 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
-and extern_notation (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation (custom,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
@@ -1066,40 +1117,43 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
-	      (match availability_of_notation (sc,ntn) allscopes with
+             (match availability_of_entry_coercion custom (fst ntn) with
+             | None -> raise No_match
+             | Some coercion ->
+               match availability_of_notation (sc,ntn) scopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes' = Option.List.cons scopt scopes in
+                  let scopes' = Option.List.cons scopt (snd scopes) in
 	          let l =
-		    List.map (fun (c,(scopt,scl)) ->
+                    List.map (fun (c,(subentry,(scopt,scl))) ->
 		      extern (* assuming no overloading: *) true
-		        (scopt,scl@scopes') vars c)
+                        (subentry,(scopt,scl@scopes')) vars c)
                       terms in
 		  let ll =
-		    List.map (fun (c,(scopt,scl)) ->
-		      List.map (extern true (scopt,scl@scopes') vars) c)
+                    List.map (fun (c,(subentry,(scopt,scl))) ->
+                      List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
                       termlists in
                   let bl =
-                    List.map (fun (bl,(scopt,scl)) ->
-                      mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl))
+                    List.map (fun (bl,(subentry,(scopt,scl))) ->
+                      mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
                       binders in
                   let bll =
-                    List.map (fun (bl,(scopt,scl)) ->
-		      pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
+                    List.map (fun (bl,(subentry,(scopt,scl))) ->
+                      pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
                       binderlists in
-                  insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)
+                  insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
           | SynDefRule kn ->
 	      let l =
-		List.map (fun (c,(scopt,scl)) ->
-		  extern true (scopt,scl@scopes) vars c, None)
+                List.map (fun (c,(subentry,(scopt,scl))) ->
+                  extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
 		  terms in
               let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
 	      CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
  	if List.is_empty args then e
 	else
-	  let args = fill_arg_scopes args argsscopes scopes in
+          let args = fill_arg_scopes args argsscopes allscopes in
 	  let args = extern_args (extern true) vars args in
 	  CAst.make ?loc @@ explicitize false argsimpls (None,e) args
       with
@@ -1113,10 +1167,10 @@ and extern_recursion_order scopes vars = function
 
 
 let extern_glob_constr vars c =
-  extern false (None,[]) vars c
+  extern false (InConstrEntrySomeLevel,(None,[])) vars c
 
 let extern_glob_type vars c =
-  extern_typ (None,[]) vars c
+  extern_typ (InConstrEntrySomeLevel,(None,[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1132,7 +1186,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
-  extern false (scopt,[]) vars r
+  extern false (InConstrEntrySomeLevel,(scopt,[])) vars r
 
 let extern_constr_in_scope goal_concl_style scope env sigma t =
   extern_constr_gen false goal_concl_style (Some scope) env sigma t
@@ -1153,7 +1207,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
   let vars = vars_of_env env in
-  extern false (None,[]) vars r
+  extern false (InConstrEntrySomeLevel,(None,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -1262,10 +1316,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
-  extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
+  extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
 
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (extended_glob_local_binder_of_decl) a in
-  pi3 (extern_local_binder (None,[]) vars a)
+  pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 715823e5d0..1c8d957014 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -218,30 +218,36 @@ let expand_notation_string ntn n =
 (* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
 (* Remark: expansion of squash at definition is done in metasyntax.ml *)
 let contract_curly_brackets ntn (l,ll,bl,bll) =
+  match ntn with
+  | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll)
+  | InConstrEntrySomeLevel, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l ->
+    | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  !ntn',(l,ll,bl,bll)
+  (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll)
 
 let contract_curly_brackets_pat ntn (l,ll) =
+  match ntn with
+  | InCustomEntryLevel _,_ -> ntn,(l,ll)
+  | InConstrEntrySomeLevel, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l ->
+    | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  !ntn',(l,ll)
+  (InConstrEntrySomeLevel,!ntn'),(l,ll)
 
 type intern_env = {
   ids: Names.Id.Set.t;
@@ -819,7 +825,7 @@ let split_by_type ids subst =
     | [] -> assert false
     | a::l -> l, Id.Map.add id (a,scl) s in
   let (terms,termlists,binders,binderlists),subst =
-    List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) ->
+    List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,((_,scl),typ)) ->
     match typ with
     | NtnTypeConstr ->
        let terms,terms' = bind id scl terms terms' in
@@ -847,10 +853,10 @@ let split_by_type ids subst =
   subst
 
 let split_by_type_pat ?loc ids subst =
-  let bind id scl l s =
+  let bind id (_,scopes) l s =
     match l with
     | [] -> assert false
-    | a::l -> l, Id.Map.add id (a,scl) s in
+    | a::l -> l, Id.Map.add id (a,scopes) s in
   let (terms,termlists),subst =
     List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) ->
     match typ with
@@ -866,7 +872,7 @@ let split_by_type_pat ?loc ids subst =
   subst
 
 let make_subst ids l =
-  let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in
+  let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
   List.fold_left2 fold Id.Map.empty ids l
 
 let intern_notation intern env ntnvars loc ntn fullargs =
@@ -1555,11 +1561,11 @@ let drop_notations_pattern looked_for genv =
         (* 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, [])
-    | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a ->
+    | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
       rcp_of_glob scopes pat
-    | CPatNotation ("( _ )",([a],[]),[]) ->
+    | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
@@ -1872,10 +1878,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	DAst.make ?loc @@
         GLetIn (na.CAst.v, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _", ([a],[],[],[])) when is_non_zero a ->
+    | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
-    | CNotation ("( _ )",([a],[],[],[])) -> intern env a
+    | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
     | CGeneralization (b,a,c) ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 5bf46282fd..ccad6b19eb 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -167,7 +167,7 @@ let dump_modref ?loc mp ty =
 let dump_libref ?loc dp ty =
   dump_ref ?loc (Names.DirPath.to_string dp) "<>" "<>" ty
 
-let cook_notation df sc =
+let cook_notation (from,df) sc =
   (* We encode notations so that they are space-free and still human-readable *)
   (* - all spaces are replaced by _                                           *)
   (* - all _ denoting a non-terminal symbol are replaced by x                 *)
@@ -203,7 +203,9 @@ let cook_notation df sc =
     if !i <= l then (set ntn !j '_'; incr j; incr i)
   done;
   let df = Bytes.sub_string ntn 0 !j in
-  match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+  let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
+  let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+  from_df_sc
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 288a0bfe00..4f3037b1fc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -98,7 +98,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (qid,_) when qualid_is_ident qid ->
       found c.CAst.loc (qualid_basename qid) bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+    | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
         qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
         Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index 05fcd0e7f5..625d072b9f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -39,6 +39,30 @@ open Context.Named.Declaration
     expression, set this scope to be the current scope
 *)
 
+let notation_entry_eq s1 s2 = match (s1,s2) with
+| InConstrEntry, InConstrEntry -> true
+| InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2
+| (InConstrEntry | InCustomEntry _), _ -> false
+
+let notation_entry_level_eq s1 s2 = match (s1,s2) with
+| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> true
+| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
+| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+
+let notation_eq (from1,ntn1) (from2,ntn2) =
+  notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
+
+let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+
+module NotationOrd =
+  struct
+    type t = notation
+    let compare = Pervasives.compare
+  end
+
+module NotationSet = Set.Make(NotationOrd)
+module NotationMap = CMap.Make(NotationOrd)
+
 (**********************************************************************)
 (* Scope of symbols *)
 
@@ -51,7 +75,7 @@ type notation_data = {
 }
 
 type scope = {
-  notations: notation_data String.Map.t;
+  notations: notation_data NotationMap.t;
   delimiters: delimiters option
 }
 
@@ -62,7 +86,7 @@ let scope_map = ref String.Map.empty
 let delimiters_map = ref String.Map.empty
 
 let empty_scope = {
-  notations = String.Map.empty;
+  notations = NotationMap.empty;
   delimiters = None
 }
 
@@ -71,6 +95,9 @@ let default_scope = "" (* empty name, not available from outside *)
 let init_scope_map () =
   scope_map := String.Map.add default_scope empty_scope !scope_map
 
+(**********************************************************************)
+(* Operations on scopes *)
+
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
   with Not_found ->
@@ -101,12 +128,12 @@ let normalize_scope sc =
 (**********************************************************************)
 (* The global stack of scopes                                         *)
 
-type scope_elem = Scope of scope_name | SingleNotation of string
+type scope_elem = Scope of scope_name | SingleNotation of notation
 type scopes = scope_elem list
 
 let scope_eq s1 s2 = match s1, s2 with
-| Scope s1, Scope s2
-| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2
+| Scope s1, Scope s2 -> String.equal s1 s2
+| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2
 | Scope _, SingleNotation _
 | SingleNotation _, Scope _ -> false
 
@@ -158,8 +185,6 @@ let push_scope sc scopes = Scope sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
-type local_scopes = tmp_scope_name option * scope_name list
-
 let make_current_scopes (tmp_scope,scopes) =
   Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
 
@@ -376,7 +401,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       end
   | SingleNotation ntn' :: scopes ->
       begin match ntn_scope, ntn with
-      | None, Some ntn when String.equal ntn ntn' ->
+      | None, Some ntn when notation_eq ntn ntn' ->
 	Some (None, None)
       | _ ->
 	find_without_delimiters find (ntn_scope,ntn) scopes
@@ -390,7 +415,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 let warn_notation_overridden =
   CWarnings.create ~name:"notation-overridden" ~category:"parsing"
                    (fun (ntn,which_scope) ->
-                    str "Notation" ++ spc () ++ str ntn ++ spc ()
+                    str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
                     ++ strbrk "was already used" ++ which_scope ++ str ".")
 
 let declare_notation_interpretation ntn scopt pat df ~onlyprint =
@@ -398,7 +423,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let sc = find_scope scope in
   if not onlyprint then begin
     let () =
-      if String.Map.mem ntn sc.notations then
+      if NotationMap.mem ntn sc.notations then
       let which_scope = match scopt with
       | None -> mt ()
       | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
@@ -408,7 +433,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
       not_interp = pat;
       not_location = df;
     } in
-    let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
+    let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
     scope_map := String.Map.add scope sc !scope_map
   end;
   begin match scopt with
@@ -425,7 +450,7 @@ let rec find_interpretation ntn find = function
   | Scope scope :: scopes ->
       (try let (pat,df) = find scope in pat,(df,Some scope)
        with Not_found -> find_interpretation ntn find scopes)
-  | SingleNotation ntn'::scopes when String.equal ntn' ntn ->
+  | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
       (try let (pat,df) = find default_scope in pat,(df,None)
        with Not_found ->
          (* e.g. because single notation only for constr, not cases_pattern *)
@@ -434,12 +459,12 @@ let rec find_interpretation ntn find = function
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
-  let n = String.Map.find ntn (find_scope sc).notations in
+  let n = NotationMap.find ntn (find_scope sc).notations in
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral (n,true) -> n
-  | Numeral (n,false) -> "- "^n
+  | Numeral (n,true) -> InConstrEntrySomeLevel, n
+  | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -459,13 +484,13 @@ let find_prim_token check_allowed ?loc p sc =
 
 let interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
-  let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
+  let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
   try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
   with Not_found ->
     user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
       | Numeral _ ->
-         str "No interpretation for numeral " ++ str (notation_of_prim_token p)
+         str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token ?loc =
@@ -490,7 +515,7 @@ let interp_notation ?loc ntn local_scopes =
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
     user_err ?loc 
-    (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
+    (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -504,9 +529,125 @@ let uninterp_ind_pattern_notations ind =
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
-    String.Map.mem ntn (String.Map.find scope !scope_map).notations in
+    NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
   find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
 
+(* We support coercions from a custom entry at some level to an entry
+   at some level (possibly the same), and from and to the constr entry. E.g.:
+
+   Notation "[ expr ]" := expr (expr custom group at level 1).
+   Notation "( x )" := x (in custom group at level 0, x at level 1).
+   Notation "{ x }" := x (in custom group at level 0, x constr).
+
+   Supporting any level is maybe overkill in that coercions are
+   commonly from the lowest level of the source entry to the highest
+   level of the target entry. *)
+
+type entry_coercion = notation list
+
+module EntryCoercionOrd =
+ struct
+  type t = notation_entry * notation_entry
+   let compare = Pervasives.compare
+ end
+
+module EntryCoercionMap = Map.Make(EntryCoercionOrd)
+
+let entry_coercion_map = ref EntryCoercionMap.empty
+
+let level_ord lev lev' =
+  match lev, lev' with
+  | None, _ -> true
+  | _, None -> true
+  | Some n, Some n' -> n <= n'
+
+let rec search nfrom nto = function
+  | [] -> raise Not_found
+  | ((pfrom,pto),coe)::l ->
+    if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l
+
+let decompose_custom_entry = function
+  | InConstrEntrySomeLevel -> InConstrEntry, None
+  | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n
+
+let availability_of_entry_coercion entry entry' =
+  let entry, lev = decompose_custom_entry entry in
+  let entry', lev' = decompose_custom_entry entry' in
+  if notation_entry_eq entry entry' && level_ord lev' lev then Some []
+  else
+    try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map))
+    with Not_found -> None
+
+let better_path ((lev1,lev2),path) ((lev1',lev2'),path') =
+  (* better = shorter and lower source and higher target *)
+  level_ord lev1 lev1' && level_ord lev2' lev2 && List.length path <= List.length path'
+
+let shorter_path (_,path) (_,path') =
+  List.length path <= List.length path'
+
+let rec insert_coercion_path path = function
+  | [] -> [path]
+  | path'::paths as allpaths ->
+      (* If better or equal we keep the more recent one *)
+      if better_path path path' then path::paths
+      else if better_path path' path then allpaths
+      else if shorter_path path path' then path::allpaths
+      else path'::insert_coercion_path path paths
+
+let declare_entry_coercion (entry,_ as ntn) entry' =
+  let entry, lev = decompose_custom_entry entry in
+  let entry', lev' = decompose_custom_entry entry' in
+  (* Transitive closure *)
+  let toaddleft =
+    EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
+        List.fold_right (fun ((lev'',lev'''),path) l ->
+        if notation_entry_eq entry entry''' && level_ord lev lev''' &&
+           not (notation_entry_eq entry' entry'')
+        then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+      !entry_coercion_map [] in
+  let toaddright =
+    EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
+        List.fold_right (fun ((lev'',lev'''),path) l ->
+        if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
+        then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+      !entry_coercion_map [] in
+  entry_coercion_map :=
+    List.fold_right (fun (pair,path) ->
+        let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
+        EntryCoercionMap.add pair (insert_coercion_path path olds))
+      (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+      !entry_coercion_map
+
+let entry_has_global_map = ref String.Map.empty
+
+let declare_custom_entry_has_global s n =
+  try
+    let p = String.Map.find s !entry_has_global_map in
+    user_err (str "Custom entry " ++ str s ++
+              str " has already a rule for global references at level " ++ int p ++ str ".")
+  with Not_found ->
+    entry_has_global_map := String.Map.add s n !entry_has_global_map
+
+let entry_has_global = function
+  | InConstrEntrySomeLevel -> true
+  | InCustomEntryLevel (s,n) ->
+     try String.Map.find s !entry_has_global_map <= n with Not_found -> false
+
+let entry_has_ident_map = ref String.Map.empty
+
+let declare_custom_entry_has_ident s n =
+  try
+    let p = String.Map.find s !entry_has_ident_map in
+    user_err (str "Custom entry " ++ str s ++
+              str " has already a rule for global references at level " ++ int p ++ str ".")
+  with Not_found ->
+    entry_has_ident_map := String.Map.add s n !entry_has_ident_map
+
+let entry_has_ident = function
+  | InConstrEntrySomeLevel -> true
+  | InCustomEntryLevel (s,n) ->
+     try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
+
 let uninterp_prim_token c =
   try
     let (sc,numpr,_) =
@@ -565,7 +706,8 @@ let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeBinderList, NtnTypeBinderList -> true
 | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
-let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
+let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+  notation_entry_level_eq entry1 entry2 &&
   pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
   ntpe_eq tp1 tp2
 
@@ -577,7 +719,7 @@ let exists_notation_in_scope scopt ntn onlyprint r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = String.Map.find scope !scope_map in
-    let n = String.Map.find ntn sc.notations in
+    let n = NotationMap.find ntn sc.notations in
     interpretation_eq n.not_interp r
   with Not_found -> false
 
@@ -793,10 +935,10 @@ let rec string_of_symbol = function
      let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
   | Break _ -> []
 
-let make_notation_key symbols =
-  String.concat " " (List.flatten (List.map string_of_symbol symbols))
+let make_notation_key from symbols =
+  (from,String.concat " " (List.flatten (List.map string_of_symbol symbols)))
 
-let decompose_notation_key s =
+let decompose_notation_key (from,s) =
   let len = String.length s in
   let rec decomp_ntn dirs n =
     if n>=len then List.rev dirs else
@@ -811,7 +953,7 @@ let decompose_notation_key s =
       | s -> Terminal (String.drop_simple_quotes s) in
     decomp_ntn (tok::dirs) (pos+1)
   in
-    decomp_ntn [] 0
+    from, decomp_ntn [] 0
 
 (************)
 (* Printing *)
@@ -840,14 +982,14 @@ let pr_notation_info prglob ntn c =
 
 let pr_named_scope prglob scope sc =
  (if String.equal scope default_scope then
-   match String.Map.cardinal sc.notations with
+   match NotationMap.cardinal sc.notations with
      | 0 -> str "No lonely notation"
      | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
   else
     str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
   ++ fnl ()
   ++ pr_scope_classes scope
-  ++ String.Map.fold
+  ++ NotationMap.fold
        (fun ntn { not_interp  = (_, r); not_location = (_, df) } strm ->
 	 pr_notation_info prglob df r ++ fnl () ++ strm)
        sc.notations (mt ())
@@ -862,11 +1004,11 @@ let pr_scopes prglob =
 let rec find_default ntn = function
   | [] -> None
   | Scope scope :: scopes ->
-    if String.Map.mem ntn (find_scope scope).notations then
+    if NotationMap.mem ntn (find_scope scope).notations then
       Some scope
     else find_default ntn scopes
   | SingleNotation ntn' :: scopes ->
-    if String.equal ntn ntn' then Some default_scope
+    if notation_eq ntn ntn' then Some default_scope
     else find_default ntn scopes
 
 let factorize_entries = function
@@ -875,7 +1017,7 @@ let factorize_entries = function
       let (ntn,l_of_ntn,rest) =
 	List.fold_left
           (fun (a',l,rest) (a,c) ->
-	    if String.equal a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
+            if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
 	  (ntn,[c],[]) l in
       (ntn,l_of_ntn)::rest
 
@@ -930,15 +1072,15 @@ let possible_notations ntn =
     (* Only "_ U _" format *)
     [ntn]
   else
-    let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in
+    let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in
     if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
 
 let browse_notation strict ntn map =
   let ntns = possible_notations ntn in
-  let find ntn' ntn =
+  let find (from,ntn' as fullntn') ntn =
     if String.contains ntn ' ' then String.equal ntn ntn'
     else
-      let toks = decompose_notation_key ntn' in
+      let _,toks = decompose_notation_key fullntn' in
       let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
       let trms = List.map_filter get_terminals toks in
       if strict then String.List.equal [ntn] trms
@@ -947,10 +1089,10 @@ let browse_notation strict ntn map =
   let l =
     String.Map.fold
       (fun scope_name sc ->
-	String.Map.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
+        NotationMap.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
           if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
-  List.sort (fun x y -> String.compare (fst x) (fst y)) l
+  List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
 
 let global_reference_of_notation test (ntn,(sc,c,_)) =
   match c with
@@ -1011,9 +1153,9 @@ let locate_notation prglob ntn scope =
 
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
-  String.Map.fold
+  NotationMap.fold
     (fun ntn { not_interp  = (_, r); not_location = (_, df) } (l,known as acc) ->
-      if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
+      if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
 
 let collect_notations stack =
@@ -1026,10 +1168,10 @@ let collect_notations stack =
 	      collect_notation_in_scope scope (find_scope scope) knownntn in
 	    ((scope,l)::all,knownntn)
       | SingleNotation ntn ->
-	  if String.List.mem ntn knownntn then (all,knownntn)
+          if List.mem_f notation_eq ntn knownntn then (all,knownntn)
 	  else
 	    let { not_interp  = (_, r); not_location = (_, df) } =
-	      String.Map.find ntn (find_scope default_scope).notations in
+              NotationMap.find ntn (find_scope default_scope).notations in
 	    let all' = match all with
 	      | (s,lonelyntn)::rest when String.equal s default_scope ->
 		  (s,(df,r)::lonelyntn)::rest
@@ -1063,15 +1205,20 @@ let pr_visibility prglob = function
 
 let freeze _ =
  (!scope_map, !scope_stack, !arguments_scope,
-  !delimiters_map, !notations_key_table, !scope_class_map)
+  !delimiters_map, !notations_key_table, !scope_class_map,
+  !entry_coercion_map, !entry_has_global_map,
+  !entry_has_ident_map)
 
-let unfreeze (scm,scs,asc,dlm,fkm,clsc) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc,coe,globs,ids) =
   scope_map := scm;
   scope_stack := scs;
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
-  scope_class_map := clsc
+  scope_class_map := clsc;
+  entry_coercion_map := coe;
+  entry_has_global_map := globs;
+  entry_has_ident_map := ids
 
 let init () =
   init_scope_map ();
diff --git a/interp/notation.mli b/interp/notation.mli
index b177b7f1e0..c921606484 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -17,6 +17,21 @@ open Notation_term
 
 (** Notations *)
 
+val pr_notation : notation -> Pp.t
+(** Printing *)
+
+val notation_entry_eq : notation_entry -> notation_entry -> bool
+(** Equality on [notation_entry]. *)
+
+val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
+(** Equality on [notation_entry_level]. *)
+
+val notation_eq : notation -> notation -> bool
+(** Equality on [notation]. *)
+
+module NotationSet : Set.S with type elt = notation
+module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+
 (** {6 Scopes } *)
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
@@ -25,8 +40,6 @@ type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
 
-type local_scopes = tmp_scope_name option * scope_name list
-
 val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
@@ -84,11 +97,11 @@ val declare_string_interpreter : scope_name -> required_module ->
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
+val interp_prim_token : ?loc:Loc.t -> prim_token -> subscopes ->
   glob_constr * (notation_location * scope_name option)
 (* This function returns a glob_const representing a pattern *)
 val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
-  local_scopes -> glob_constr * (notation_location * scope_name option)
+  subscopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
@@ -101,7 +114,7 @@ val uninterp_prim_token_ind_pattern :
  inductive -> cases_pattern list -> scope_name * prim_token
 
 val availability_of_prim_token :
-  prim_token -> scope_name -> local_scopes -> delimiters option option
+  prim_token -> scope_name -> subscopes -> delimiters option option
 
 (** {6 Declare and interpret back and forth a notation } *)
 
@@ -116,7 +129,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (** Return the interpretation bound to a notation *)
-val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
+val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
 type notation_rule = interp_rule * interpretation * int option
@@ -129,13 +142,13 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
    argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> local_scopes ->
+val availability_of_notation : scope_name option * notation -> subscopes ->
   (scope_name option * delimiters option) option
 
 (** {6 Miscellaneous} *)
 
 val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
-      notation -> delimiters option -> GlobRef.t
+      notation_key -> delimiters option -> GlobRef.t
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
@@ -177,8 +190,8 @@ type symbol =
 val symbol_eq : symbol -> symbol -> bool
 
 (** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : symbol list -> notation
-val decompose_notation_key : notation -> symbol list
+val make_notation_key : notation_entry_level -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry_level * symbol list
 
 (** Decompose a notation of the form "a 'U' b" *)
 val decompose_raw_notation : string -> symbol list
@@ -187,11 +200,21 @@ val decompose_raw_notation : string -> symbol list
 val pr_scope_class : scope_class -> Pp.t
 val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
 val pr_scopes : (glob_constr -> Pp.t) -> Pp.t
-val locate_notation : (glob_constr -> Pp.t) -> notation ->
+val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
       scope_name option -> Pp.t
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
+type entry_coercion = notation list
+val declare_entry_coercion : notation -> notation_entry_level -> unit
+val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
+
+val declare_custom_entry_has_global : string -> int -> unit
+val declare_custom_entry_has_ident : string -> int -> unit
+
+val entry_has_global : notation_entry_level -> bool
+val entry_has_ident : notation_entry_level -> bool
+
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7cde563cd2..06943ce7b9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1008,9 +1008,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
 let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
   (terms,termlists,binders,Id.List.remove_assoc x binderlists)
 
-let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
+let add_ldots_var metas = (ldots_var,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas
 
-let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+let add_meta_bindinglist x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeBinderList))::metas
 
 (* This tells if letins in the middle of binders should be included in
    the sequence of binders *)
@@ -1055,7 +1055,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
   match_fun alp metas sigma rest termin
 
-let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
+let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
 
 let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma acc rest =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f038b5be1a..58fa221b16 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,18 +53,18 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
 exception No_match
 
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
-      ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
-      ('a cases_pattern_disjunction_g * subscopes) list *
-      ('a extended_glob_local_binder_g list * subscopes) list
+      ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
+      ('a cases_pattern_disjunction_g * extended_subscopes) list *
+      ('a extended_glob_local_binder_g list * extended_subscopes) list
 
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6d9effcef4..942ea5ff3f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -58,6 +58,8 @@ type tmp_scope_name = scope_name
 
 type subscopes = tmp_scope_name option * scope_name list
 
+type extended_subscopes = Constrexpr.notation_entry_level * subscopes
+
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
 
@@ -86,7 +88,7 @@ type notation_var_internalization_type =
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
-    (Id.t * (subscopes * notation_var_instance_type)) list *
+    (Id.t * (extended_subscopes * notation_var_instance_type)) list *
     notation_constr
 
 type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a4f20fd739..e3d490a1ad 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -77,8 +77,8 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 
 (* Coercions to the general format of notation that also supports
    variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
+let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
+let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
 
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
diff --git a/parsing/extend.ml b/parsing/extend.ml
index f57e32c884..a3e27f9cf5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -38,10 +38,8 @@ type 'a constr_entry_key_gen =
   | ETReference
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of 'a
-  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
-  | ETOther of string * string
 
 (** Entries level (left-hand side of grammar rules) *)
 
@@ -63,9 +61,8 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
   | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
   | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index b2913d5d4f..49e1cd7ec9 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -225,11 +225,11 @@ GRAMMAR EXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
         { (match c.CAst.v with
             | CPrim (Numeral (n,true)) ->
-                CAst.make ~loc @@ CNotation("( _ )",([c],[],[],[]))
+                CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; "|}" -> { c }
       | "{"; c = binder_constr ; "}" ->
-          { CAst.make ~loc @@ CNotation(("{ _ }"),([c],[],[],[])) }
+          { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -411,13 +411,13 @@ GRAMMAR EXTEND Gram
       | "("; p = pattern LEVEL "200"; ")" ->
           { (match p.CAst.v with
             | CPatPrim (Numeral (n,true)) ->
-                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+                 CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p) }
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           { let p =
             match p with
             | { CAst.v = CPatPrim (Numeral (n,true)) } ->
-                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+                 CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc @@ CPatCast (p, ty) }
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 346350641f..d8c08803b6 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -17,7 +17,8 @@ type precedence = int
 type parenRelation = L | E | Any | Prec of precedence
 type tolerability = precedence * parenRelation
 
-type level = precedence * tolerability list * constr_entry_key list
+type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+  (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 071e6db205..125ea01681 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -11,55 +11,59 @@
 open Pp
 open CErrors
 open Util
-open Extend
+open Notation
 open Notation_gram
 
 (* Uninterpreted notation levels *)
 
-let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
 let declare_notation_level ?(onlyprint=false) ntn level =
-  if String.Map.mem ntn !notation_level_map then
-    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
-  notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
+  if NotationMap.mem ntn !notation_level_map then
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.");
+  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
 
 let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
   if onlyprint' && not onlyprint then raise Not_found;
   level
 
 (**********************************************************************)
-(* Operations on scopes *)
+(* Equality *)
+
+open Extend
 
 let parenRelation_eq t1 t2 = match t1, t2 with
 | L, L | E, E | Any, Any -> true
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let production_level_eq l1 l2 = true (* (l1 = l2) *)
+let production_position_eq pp1 pp2 = match (pp1,pp2) with
+| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
+| InternalProd, InternalProd -> true
+| (BorderProd _ | InternalProd), _ -> false
 
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+let production_level_eq l1 l2 = match (l1,l2) with
 | NextLevel, NextLevel -> true
 | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
+| (NextLevel | NumLevel _), _ -> false
 
 let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETName, ETName -> true
 | ETReference, ETReference -> true
 | ETBigint, ETBigint -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
+   notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
   let prod_eq (l1,pp1) (l2,pp2) =
-    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
-    else production_level_eq l1 l2 in
-  Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+    not strict ||
+    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
+  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
   && List.equal (constr_entry_key_eq prod_eq) u1 u2
 
 let level_eq = level_eq_gen false
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9d2f73eeb8..8455992f20 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -560,15 +560,34 @@ let register_grammars_by_name name grams =
 let find_grammars_by_name name =
   String.Map.find name !grammar_names
 
+(** Custom entries *)
+
+let custom_entries = ref String.Map.empty
+
+let create_custom_entries s =
+  let sc = "constr:"^s in
+  let sp = "pattern:"^s in
+  let c = (Gram.entry_create sc : Constrexpr.constr_expr Gram.entry) in
+  let p = (Gram.entry_create sp : Constrexpr.cases_pattern_expr Gram.entry) in
+  register_grammars_by_name s [AnyEntry c; AnyEntry p];
+  custom_entries := String.Map.add s (c,p) !custom_entries
+
+let find_custom_entries s =
+  try String.Map.find s !custom_entries
+  with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+
 (** Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
 type frozen_t =
   (int * GrammarCommand.t * GramState.t) list *
   CLexer.keyword_state *
-  any_entry list String.Map.t
+  any_entry list String.Map.t *
+  (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry) Util.String.Map.t
 
-let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state (), !grammar_names)
+let freeze _ : frozen_t =
+  (!grammar_stack, CLexer.get_keyword_state (),
+   !grammar_names, !custom_entries)
 
 (* We compare the current state of the grammar and the state to unfreeze,
    by computing the longest common suffixes *)
@@ -578,14 +597,15 @@ let factorize_grams l1 l2 =
 let number_of_entries gcl =
   List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
 
-let unfreeze (grams, lex, names) =
+let unfreeze (grams, lex, names, custom) =
   let (undo, redo, common) = factorize_grams !grammar_stack grams in
   let n = number_of_entries undo in
   remove_grammars n;
   grammar_stack := common;
   CLexer.set_keyword_state lex;
   List.iter extend_dyn_grammar (List.rev_map pi2 redo);
-  grammar_names := names
+  grammar_names := names;
+  custom_entries := custom
 
 (** No need to provide an init function : the grammar state is
     statically available, and already empty initially, while
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 029c437136..9711cd0461 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -272,3 +272,8 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
+
+(** Create a custom entry of some name *)
+
+val create_custom_entries : string -> unit
+val find_custom_entries : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index d2b50fa83d..e1f5e20117 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -11,6 +11,7 @@
 open Util
 open Pp
 open CErrors
+open Notation
 open Notation_gram
 
 (*s Pretty-print. *)
@@ -48,29 +49,29 @@ type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let notation_rules =
-  Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+  Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
 
 let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+  notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
 
 let find_notation_printing_rule ntn =
-  try pi1 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+  try pi1 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
 let find_notation_extra_printing_rules ntn =
-  try pi2 (String.Map.find ntn !notation_rules)
+  try pi2 (NotationMap.find ntn !notation_rules)
   with Not_found -> []
 let find_notation_parsing_rules ntn =
-  try pi3 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+  try pi3 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
 
 let get_defined_notations () =
-  String.Set.elements @@ String.Map.domain !notation_rules
+  NotationSet.elements @@ NotationMap.domain !notation_rules
 
 let add_notation_extra_printing_rule ntn k v =
   try
     notation_rules :=
-      let p, pp, gr = String.Map.find ntn !notation_rules in
-      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+      let p, pp, gr = NotationMap.find ntn !notation_rules in
+      NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
     user_err ~hdr:"add_notation_extra_printing_rule"
       (str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 9f61e121a4..7eb5967a3e 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,7 +41,6 @@ type unparsing =
 
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-
 val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 8ce0316f53..989a6c5bf1 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -217,8 +217,8 @@ let interp_search_notation ?loc tag okey =
          (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
       else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
     loop 0 1 in
-  let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in
-  let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in
+  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
   let pr_and_list pr = function
     | [x] -> pr x
     | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
@@ -293,7 +293,7 @@ let interp_search_notation ?loc tag okey =
     let scs' = List.remove (=) sc !scs in
     let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
     Feedback.msg_warning (hov 4 w)
-  else if String.string_contains ~where:ntn ~what:" .. " then
+  else if String.string_contains ~where:(snd ntn) ~what:" .. " then
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 05eda14e90..30a998c6ce 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -929,7 +929,7 @@ let glob_cpattern gs p =
   | k, (v, Some t), _ as orig ->
      if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
      match t.CAst.v with
-     | CNotation("( _ in _ )", ([t1; t2], [], [], [])) ->
+     | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
          (try match glob t1, glob t2 with
          | (r1, None), (r2, None) -> encode k "In" [r1;r2]
          | (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -937,11 +937,11 @@ let glob_cpattern gs p =
          | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
          | _ -> CErrors.anomaly (str"where are we?.")
          with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
-     | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) ->
+     | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
-     | CNotation("( _ as _ )", ([t1; t2], [], [], [])) ->
+     | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
          encode k "As" [fst (glob t1); fst (glob t2)]
-     | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) ->
+     | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
      | _ -> glob_ssrterm gs orig
 ;;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e38da45b95..418e13759b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -295,7 +295,7 @@ let tag_var = tag Tag.variable
       | CPatOr pl ->
         hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
 
-      | CPatNotation ("( _ )",([p],[]),[]) ->
+      | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
         pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
 
       | CPatNotation (s,(l,ll),args) ->
@@ -665,7 +665,7 @@ let tag_var = tag Tag.variable
                     | CastCoerce -> str ":>"),
           lcast
         )
-      | CNotation ("( _ )",([t],[],[],[])) ->
+      | CNotation ((_,"( _ )"),([t],[],[],[])) ->
         return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
       | CNotation (s,env) ->
         pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index eca0c6674b..a9a27e8100 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -169,7 +169,7 @@ let classify_vernac e =
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-    | VernacSyntaxExtension _
+    | VernacSyntaxExtension _ | VernacDeclareCustomEntry _
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index 5e4b676c2f..d2d4d5d764 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -60,32 +60,32 @@ Various checks for coqdoc
 <span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). 
+<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">&quot;</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
+<span class="id" title="keyword">Notation</span> <a name="f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">&quot;</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">&quot;</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
+<span class="id" title="keyword">Notation</span> <a name="a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">&quot;</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">&quot;</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/>
+<span class="id" title="keyword">Notation</span> <a name="3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">&quot;</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/>
 
 <br/>
-<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/>
+<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:&gt;</span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/>
 <br/>
-<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
+<span class="id" title="keyword">where</span> <a name="b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">&quot;</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">&quot;</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/>
@@ -97,7 +97,7 @@ Various checks for coqdoc
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">&quot;</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">&quot;</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/>
 
 <br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/>
@@ -106,19 +106,19 @@ Various checks for coqdoc
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">Admitted</span>.<br/>
 
 <br/>
@@ -137,7 +137,7 @@ Various checks for coqdoc
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
 
 <br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/>
 
 <br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/>
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index f42db99dc2..24f96ff1e6 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -51,34 +51,34 @@ Various checks for coqdoc
 \coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
+\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
 \coqdocnoindent
 \coqdoceol
 \coqdocnoindent
-\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.:::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
 \coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol
@@ -90,7 +90,7 @@ Various checks for coqdoc
 \coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.test.::my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.:::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
 \coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol
@@ -99,19 +99,19 @@ Various checks for coqdoc
 \coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
-\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{::type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
 \coqdocindent{2.00em}
 \coqdocvar{Admitted}.\coqdoceol
 \coqdocemptyline
@@ -131,7 +131,7 @@ Various checks for coqdoc
 \coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
 \coqdocemptyline
 \coqdocindent{3.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
 \coqdocemptyline
 \coqdocindent{2.00em}
 \coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
new file mode 100644
index 0000000000..cef7d1a702
--- /dev/null
+++ b/test-suite/output/Notations4.out
@@ -0,0 +1,17 @@
+[< 0 > + < 1 > * < 2 >]
+     : nat
+[<< # 0 >>]
+     : option nat
+[1 {f 1}]
+     : Expr
+fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
+     : nat -> Expr -> Expr -> Expr
+fun e : Expr =>
+match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| _ => [e + e]
+end
+     : Expr -> Expr
+[(1 + 1)]
+     : Expr
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
new file mode 100644
index 0000000000..9738ce5a5e
--- /dev/null
+++ b/test-suite/output/Notations4.v
@@ -0,0 +1,68 @@
+(* An example with constr subentries *)
+
+Module A.
+
+Declare Custom Entry myconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
+Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
+Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
+Check [ < 0 > + < 1 > * < 2 >].
+
+Declare Custom Entry anotherconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10).
+Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
+Check [ << # 0 >> ].
+
+End A.
+
+Module B.
+
+Inductive Expr :=
+ | Mul : Expr -> Expr -> Expr
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 2).
+Notation "1" := One (in custom expr at level 0).
+Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+Notation "{ x }" := x (in custom expr at level 0, x constr).
+Notation "x" := x (in custom expr at level 0, x ident).
+
+Axiom f : nat -> Expr.
+Check [1 {f 1}].
+Check fun x y z => [1 + y z + {f x}].
+Check fun e => match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| y => [y + e]
+end.
+
+End B.
+
+Module C.
+
+Inductive Expr :=
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 1).
+Notation "1" := One (in custom expr at level 0).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+
+(* Check the use of a two-steps coercion from constr to expr 1 then
+   from expr 0 to expr 2 (note that camlp5 parsing is more tolerant
+   and does not require parentheses to parse from level 2 while at
+   level 1) *)
+
+Check [1 + 1].
+
+End C.
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index fa2393b910..32cfb354bf 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -1,35 +1,35 @@
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ - _ was already used in scope nat_scope.
+Warning: Notation "_ - _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ >= _ was already used in scope nat_scope.
+Warning: Notation "_ >= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ > _ was already used in scope nat_scope.
+Warning: Notation "_ > _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ + _ was already used in scope nat_scope.
+Warning: Notation "_ + _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ * _ was already used in scope nat_scope.
+Warning: Notation "_ * _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 BEGIN INSTANCES
 instance: (x + y + z) matches: (x + y + z)
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 885324aa02..724d3838b0 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -185,7 +185,8 @@ let type_name = function
 let prepare_entry s = function
   | Notation ->
       (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
-      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
+      (* Encoded notations have the form section:entry:sc:x_'++'_x       *)
+      (* where:                                                          *)
       (* - the section, if any, ends with a "."                          *)
       (* - the scope can be empty                                        *)
       (* - tokens are separated with "_"                                 *)
@@ -202,10 +203,12 @@ let prepare_entry s = function
       let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
-      let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = Bytes.make (String.length s - i) ' ' in
+      let m = try String.index_from s (i+1) ':' with _ -> err () in
+      let entry = String.sub s (h+1) (i-h-1) in
+      let sc = String.sub s (i+1) (m-i-1) in
+      let ntn = Bytes.make (String.length s - m) ' ' in
       let k = ref 0 in
-      let j = ref (i+1) in
+      let j = ref (m+1) in
       let quoted = ref false in
       let l = String.length s - 1 in
       while !j <= l do
@@ -227,7 +230,8 @@ let prepare_entry s = function
 	incr j
       done;
       let ntn = Bytes.sub_string ntn 0 !k in
-      if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
+      let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in
+      if entry = "" then ntn else entry ^ ":" ^ ntn
   | _ ->
       s
 
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 3281b75aaa..65e5f4bede 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -54,6 +54,17 @@ let default_pattern_levels =
 
 let default_constr_levels = (default_levels, default_pattern_levels)
 
+let find_levels levels = function
+  | InConstrEntry -> levels, String.Map.find "constr" levels
+  | InCustomEntry s ->
+     try levels, String.Map.find s levels
+     with Not_found ->
+     String.Map.add s ([],[]) levels, ([],[])
+
+let save_levels levels custom lev =
+  let s = match custom with InConstrEntry -> "constr" | InCustomEntry s -> s in
+  String.Map.add s lev levels
+
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
 (* first LeftA, then RightA and NoneA together *)
@@ -125,24 +136,24 @@ let rec list_mem_assoc_triple x = function
 let register_empty_levels accu forpat levels =
   let rec filter accu = function
   | [] -> ([], accu)
-  | n :: rem ->
+  | (where,n) :: rem ->
     let rem, accu = filter accu rem in
-    let (clev, plev) = accu in
+    let accu, (clev, plev) = find_levels accu where in
     let levels = if forpat then plev else clev in
     if not (list_mem_assoc_triple n levels) then
       let nlev, ans = find_position_gen levels true None (Some n) in
       let nlev = if forpat then (clev, nlev) else (nlev, plev) in
-      ans :: rem, nlev
+      (where, ans) :: rem, save_levels accu where nlev
     else rem, accu
   in
   filter accu levels
 
-let find_position accu forpat assoc level =
-  let (clev, plev) = accu in
+let find_position accu custom forpat assoc level =
+  let accu, (clev, plev) = find_levels accu custom in
   let levels = if forpat then plev else clev in
   let nlev, ans = find_position_gen levels false assoc level in
   let nlev = if forpat then (clev, nlev) else (nlev, plev) in
-  (ans, nlev)
+  (ans, save_levels accu custom nlev)
 
 (**************************************************************************)
 (*
@@ -231,7 +242,7 @@ type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTConstr : prod_info * 'r target -> ('r, 'r) entry
+| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -240,16 +251,31 @@ type (_, _) entry =
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
 (* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
-  fun forpat level -> match forpat with
+let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
+  fun custom forpat level ->
+  match custom with
+  | InCustomEntry s ->
+     (let (entry_for_constr, entry_for_patttern) = find_custom_entries s in
+     match forpat with
+     | ForConstr -> entry_for_constr, Some level
+     | ForPattern -> entry_for_patttern, Some level)
+  | InConstrEntry ->
+  match forpat with
   | ForConstr ->
     if level = 200 then Constr.binder_constr, None
     else Constr.operconstr, Some level
   | ForPattern -> Constr.pattern, Some level
 
-let target_entry : type s. s target -> s Entry.t = function
-| ForConstr -> Constr.operconstr
-| ForPattern -> Constr.pattern
+let target_entry : type s. notation_entry -> s target -> s Entry.t = function
+| InConstrEntry ->
+   (function
+   | ForConstr -> Constr.operconstr
+   | ForPattern -> Constr.pattern)
+| InCustomEntry s ->
+   let (entry_for_constr, entry_for_patttern) = find_custom_entries s in
+   function
+   | ForConstr -> entry_for_constr
+   | ForPattern -> entry_for_patttern
 
 let is_self from e = match e with
 | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
@@ -273,11 +299,11 @@ let make_sep_rules = function
   let r = mkrule (List.rev tkl) in
   Arules [r]
 
-let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
-  if is_binder_level from p then Aentryl (target_entry forpat, "200")
+let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat ->
+  if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200")
   else if is_self from p then Aself
   else
-    let g = target_entry forpat in
+    let g = target_entry custom forpat in
     let lev = adjust_level assoc from p in
     begin match lev with
     | None -> Aentry g
@@ -286,11 +312,11 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
-| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat
+| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
 | TTConstrList (typ', [], forpat) ->
-  Alist1 (symbol_of_target typ' assoc from forpat)
+  Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat)
 | TTConstrList (typ', tkl, forpat) ->
-  Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+  Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl)
 | TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
@@ -303,9 +329,8 @@ let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
-| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
-| ETProdOther _ -> assert false (** not used *)
 | ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
 | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
 | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
@@ -420,21 +445,23 @@ let target_to_bool : type r. r target -> bool = function
 | ForConstr -> false
 | ForPattern -> true
 
-let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
+let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
-  if forpat then ExtendRule (Constr.pattern, reinit, empty)
-  else ExtendRule (Constr.operconstr, reinit, empty)
-
-let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
-| Stop -> []
-| Next (rem, Aentryl (_, i)) ->
-  let i = int_of_string i in
-  let rem = pure_sublevels level rem in
-  begin match level with
-  | Some j when Int.equal i j -> rem
-  | _ -> i :: rem
-  end
-| Next (rem, _) -> pure_sublevels level rem
+  ExtendRule (target_entry where forpat, reinit, empty)
+
+let rec pure_sublevels' custom assoc from forpat level = function
+| [] -> []
+| GramConstrNonTerminal (e,_) :: rem ->
+   let rem = pure_sublevels' custom assoc from forpat level rem in
+   let push where p rem =
+     match symbol_of_target custom p assoc from forpat with
+     | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+     | _ -> rem in
+   (match e with
+   | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
+   | ETProdConstr (s,p) -> push s p rem
+   | _ -> rem)
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
@@ -445,17 +472,17 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   CAst.make ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
-  let n,_,_ = ng.notgram_level in
+  let custom,n,_,_ = ng.notgram_level in
   let assoc = ng.notgram_assoc in
-  let (entry, level) = interp_constr_entry_key forpat n in
+  let (entry, level) = interp_constr_entry_key custom forpat n in
   let fold (accu, state) pt =
     let AnyTyRule r = make_ty_rule assoc n forpat pt in
     let symbs = ty_erase r in
-    let pure_sublevels = pure_sublevels level symbs in
+    let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
-    let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
-    let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
+    let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
+    let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
     let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule = (name, p4assoc, [Rule (symbs, act)]) in
@@ -468,7 +495,7 @@ let constr_levels = GramState.field ()
 
 let extend_constr_notation ng state =
   let levels = match GramState.get state constr_levels with
-  | None -> default_constr_levels
+  | None -> String.Map.add "constr" default_constr_levels String.Map.empty
   | Some lev -> lev
   in
   (* Add the notation in constr *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a35a1998d3..2e777d9602 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1087,6 +1087,11 @@ GRAMMAR EXTEND Gram
          r = red_expr ->
 	   { VernacDeclareReduction (s,r) }
 
+(* factorized here, though relevant for syntax extensions *)
+
+      | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
+           { VernacDeclareCustomEntry s }
+
  ] ];
     END
 
@@ -1153,6 +1158,9 @@ GRAMMAR EXTEND Gram
   ;
   syntax_modifier:
     [ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
+      | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
+      | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
+         { SetCustomEntry (x,Some n) }
       | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
       | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
       | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
@@ -1166,10 +1174,11 @@ GRAMMAR EXTEND Gram
           | { 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,lev) }
-      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],lev) }
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,Some lev) }
-      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,None) }
+        lev = level -> { SetItemLevel (x::l,None,Some lev) }
+      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
+        { SetItemLevel ([x],Some b,Some lev) }
+      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
       | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
     ] ]
   ;
@@ -1177,12 +1186,15 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "ident" -> { ETName } | IDENT "global" -> { ETReference }
       | IDENT "bigint" -> { ETBigint }
       | IDENT "binder" -> { ETBinder true }
-      | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> { ETConstrAsBinder (b,n) }
+      | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
+      | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
       | IDENT "pattern" -> { ETPattern (false,None) }
       | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
       | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
       | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
       | IDENT "closed"; IDENT "binder" -> { ETBinder false }
+      | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+           { ETConstr (InCustomEntry x,b,n) }
     ] ]
   ;
   at_level:
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 33e6229b29..9956c1546d 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -283,20 +283,30 @@ let error_not_same_scope x y =
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
 
+let pr_notation_entry = function
+  | InConstrEntry -> str "constr"
+  | InCustomEntry s -> str "custom " ++ str s
+
 let prec_assoc = function
   | RightA -> (L,E)
   | LeftA -> (E,L)
   | NonA -> (L,L)
 
-let precedence_of_position_and_level from = function
+let precedence_of_position_and_level from_level = function
   | NumLevel n, BorderProd (_,None) -> n, Prec n
   | NumLevel n, BorderProd (b,Some a) ->
       n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
   | NumLevel n, InternalProd -> n, Prec n
-  | NextLevel, _ -> from, L
-
-let precedence_of_entry_type from = function
-  | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x
+  | NextLevel, _ -> from_level, L
+
+let precedence_of_entry_type (from_custom,from_level) = function
+  | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
+    precedence_of_position_and_level from_level x
+  | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+  | ETConstr (custom,_,(NextLevel,_)) ->
+    user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
+              quote (pr_notation_entry custom) ++ strbrk " is different from " ++
+              quote (pr_notation_entry from_custom) ++ str ").")
   | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
   | _ -> 0, E (* should not matter *)
 
@@ -367,15 +377,14 @@ let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
   let prec = snd (precedence_of_entry_type from x) in
   match x with
-  | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint ->
+  | ETConstr _ | ETReference | ETBigint ->
      UnpMetaVar (i,prec)
   | ETPattern _ ->
      UnpBinderMetaVar (i,prec)
   | ETName ->
-     UnpBinderMetaVar (i,Prec 0)
+     UnpBinderMetaVar (i,prec)
   | ETBinder isopen ->
      assert false
-  | ETOther _ -> failwith "TODO"
 
 (* Heuristics for building default printing rules *)
 
@@ -561,11 +570,10 @@ let hunks_of_format (from,(vars,typs)) symfmt =
 (**********************************************************************)
 (* Build parsing rules                                                *)
 
-let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
+let assoc_of_type from n (_,typ) = precedence_of_entry_type (from,n) typ
 
 let is_not_small_constr = function
     ETProdConstr _ -> true
-  | ETProdOther("constr","binder_constr") -> true
   | _ -> false
 
 let rec define_keywords_aux = function
@@ -595,9 +603,9 @@ let distribute a ll = List.map (fun l -> a @ l) ll
      t;sep;t;...;t;sep;t;...;t;sep;t (p+n times)
      t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *)
 
-let expand_list_rule typ tkl x n p ll =
+let expand_list_rule s typ tkl x n p ll =
   let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in
-  let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in
+  let main = GramConstrNonTerminal (ETProdConstr (s,typ), camlp5_message_name) in
   let tks = List.map (fun x -> GramConstrTerminal x) tkl in
   let rec aux i hds ll =
   if i < p then aux (i+1) (main :: tks @ hds) ll
@@ -613,7 +621,7 @@ let expand_list_rule typ tkl x n p ll =
 
 let is_constr_typ typ x etyps =
   match List.assoc x etyps with
-  | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ'
+  | ETConstr (_,_,typ') -> typ = typ'
   | _ -> false
 
 let include_possible_similar_trailing_pattern typ etyps sl l =
@@ -631,9 +639,8 @@ let prod_entry_type = function
   | ETReference -> ETProdReference
   | ETBigint -> ETProdBigint
   | ETBinder _ -> assert false (* See check_binder_type *)
-  | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p
+  | ETConstr (s,_,p) -> ETProdConstr (s,p)
   | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
-  | ETOther (s,t) -> ETProdOther (s,t)
 
 let make_production etyps symbols =
   let rec aux = function
@@ -651,9 +658,9 @@ let make_production etyps symbols =
             | Break _ -> []
             | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
 	match List.assoc x etyps with
-        | ETConstr typ ->
+        | ETConstr (s,_,typ) ->
             let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
-            expand_list_rule typ tkl x 1 p (aux l')
+            expand_list_rule s typ tkl x 1 p (aux l')
         | ETBinder o ->
             check_open_binder o sl x;
             let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in
@@ -675,8 +682,7 @@ let rec find_symbols c_current c_next c_last = function
       (x,c_next)::(find_symbols c_next c_next c_last sl')
 
 let border = function
-  | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
-  | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a
+  | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a
   | _ -> None
 
 let recompute_assoc typs =
@@ -698,23 +704,24 @@ let pr_arg_level from (lev,typ) =
   | (n,_) -> str "Unknown level" in
   Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
   (match typ with
-   | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev
+   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
    | _ -> mt ())
 
-let pr_level ntn (from,args,typs) =
-  str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
-  prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs)
+let pr_level ntn (from,fromlevel,args,typs) =
+  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
 
 let error_incompatible_level ntn oldprec prec =
   user_err 
-    (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++
+    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
 
 let error_parsing_incompatible_level ntn ntn' oldprec prec =
   user_err
-    (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++
+    (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
     str " which is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
@@ -738,7 +745,7 @@ type syntax_extension_obj = locality_flag * syntax_extension
 let check_and_extend_constr_grammar ntn rule =
   try
     let ntn_for_grammar = rule.notgram_notation in
-    if String.equal ntn ntn_for_grammar then raise Not_found;
+    if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
     let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
     if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
@@ -760,7 +767,7 @@ let cache_one_syntax_extension se =
       if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
       (* Declare the notation rule *)
       declare_notation_rule ntn
-        ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
+        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
     end
 
 let cache_syntax_extension (_, (_, sy)) =
@@ -797,7 +804,9 @@ module NotationMods = struct
 type notation_modifier = {
   assoc         : gram_assoc option;
   level         : int option;
+  custom        : notation_entry;
   etyps         : (Id.t * simple_constr_prod_entry_key) list;
+  subtyps       : (Id.t * production_level) list;
 
   (* common to syn_data below *)
   only_parsing  : bool;
@@ -810,7 +819,9 @@ type notation_modifier = {
 let default = {
   assoc         = None;
   level         = None;
+  custom        = InConstrEntry;
   etyps         = [];
+  subtyps       = [];
   only_parsing  = false;
   only_printing = false;
   compat        = None;
@@ -821,53 +832,75 @@ let default = {
 end
 
 let interp_modifiers modl = let open NotationMods in
-  let rec interp acc = function
-    | [] -> acc
+  let rec interp subtyps acc = function
+    | [] -> subtyps, acc
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id acc.etyps then
 	  user_err ~hdr:"Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
-        interp { acc with etyps = (id,typ) :: acc.etyps; } l
-    | SetItemLevel ([],n) :: l ->
-        interp acc l
-    | SetItemLevelAsBinder ([],_,_) :: l ->
-        interp acc l
-    | SetItemLevel (s::idl,n) :: l ->
+        interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l
+    | SetItemLevel ([],bko,n) :: l ->
+        interp subtyps acc l
+    | SetItemLevel (s::idl,bko,n) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id acc.etyps then
 	  user_err ~hdr:"Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
-        let typ = ETConstr (Some n) in
-        interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
-    | SetItemLevelAsBinder (s::idl,bk,n) :: l ->
-        let id = Id.of_string s in
-        if Id.List.mem_assoc id acc.etyps then
-          user_err ~hdr:"Metasyntax.interp_modifiers"
-            (str s ++ str " is already assigned to an entry or constr level.");
-        let typ = ETConstrAsBinder (bk,n) in
-        interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
+        interp ((id,bko,n)::subtyps) acc (SetItemLevel (idl,bko,n)::l)
     | SetLevel n :: l ->
-        interp { acc with level = Some n; } l
+        (match acc.custom with
+        | InCustomEntry s ->
+          if acc.level <> None then
+            user_err (str ("isolated \"at level " ^ string_of_int n ^ "\" unexpected."))
+          else
+            user_err (str ("use \"in custom " ^ s ^ " at level " ^ string_of_int n ^
+                         "\"") ++ spc () ++ str "rather than" ++ spc () ++
+                         str ("\"at level " ^ string_of_int n ^ "\"") ++
+                         spc () ++ str "isolated.")
+        | InConstrEntry ->
+          if acc.level <> None then
+            user_err (str "A level is already assigned.");
+          interp subtyps { acc with level = Some n; } l)
+    | SetCustomEntry (s,n) :: l ->
+        if acc.level <> None then
+          (if n = None then
+            user_err (str ("use \"in custom " ^ s ^ " at level " ^
+                         string_of_int (Option.get acc.level) ^
+                         "\"") ++ spc () ++ str "rather than" ++ spc () ++
+                         str ("\"at level " ^
+                         string_of_int (Option.get acc.level) ^ "\"") ++
+                         spc () ++ str "isolated.")
+          else
+            user_err (str ("isolated \"at level " ^ string_of_int (Option.get acc.level) ^ "\" unexpected.")));
+        if acc.custom <> InConstrEntry then
+           user_err (str "Entry is already assigned to custom " ++ str s ++ (match acc.level with None -> mt () | Some lev -> str " at level " ++ int lev) ++ str ".");
+        interp subtyps { acc with custom = InCustomEntry s; level = n } l
     | SetAssoc a :: l ->
 	if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
-        interp { acc with assoc = Some a; } l
+        interp subtyps { acc with assoc = Some a; } l
      | SetOnlyParsing :: l ->
-        interp { acc with only_parsing = true; } l
+        interp subtyps { acc with only_parsing = true; } l
     | SetOnlyPrinting :: l ->
-        interp { acc with only_printing = true; } l
+        interp subtyps { acc with only_printing = true; } l
     | SetCompatVersion v :: l ->
-        interp { acc with compat = Some v; } l
+        interp subtyps { acc with compat = Some v; } l
     | SetFormat ("text",s) :: l ->
 	if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
-        interp { acc with format = Some s; } l
-    | SetFormat (k,{CAst.v=s}) :: l ->
-        interp { acc with extra = (k,s)::acc.extra; } l
-  in interp default modl
+        interp subtyps { acc with format = Some s; } l
+    | SetFormat (k,s) :: l ->
+        interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
+  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
+  { mods with etyps = extra_etyps@mods.etyps }
 
 let check_infix_modifiers modifiers =
-  let t = (interp_modifiers modifiers).NotationMods.etyps in
-  if not (List.is_empty t) then
+  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
     user_err Pp.(str "Explicit entry level or type unexpected in infix notation.")
 
 let check_useless_entry_types recvars mainvars etyps =
@@ -908,21 +941,18 @@ let get_compat_version mods =
 
 (* Compute precedences from modifiers (or find default ones) *)
 
-let set_entry_type etyps (x,typ) =
+let set_entry_type from etyps (x,typ) =
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (Some n), (_,BorderProd (left,_)) ->
-          ETConstr (n,BorderProd (left,None))
-      | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
-      | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) ->
-          ETConstrAsBinder (bk, (n,BorderProd (left,None)))
-      | ETConstrAsBinder (bk, Some n), (_,InternalProd) ->
-         ETConstrAsBinder (bk, (n,InternalProd))
+      | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+          ETConstr (s,bko,(n,BorderProd (left,None)))
+      | ETConstr (s,bko,Some n), (_,InternalProd) ->
+         ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x
-      | ETConstr None, _ -> ETConstr typ
-      | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ)
-    with Not_found -> ETConstr typ
+      | (ETName | ETBigint | ETReference | ETBinder _ as x), _ -> x
+      | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
+    with Not_found ->
+      ETConstr (from,None,typ)
   in (x,typ)
 
 let join_auxiliary_recursive_types recvars etyps =
@@ -942,8 +972,8 @@ let join_auxiliary_recursive_types recvars etyps =
 
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
-  | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference
-  | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
+  | ETConstr _ | ETBigint | ETReference
+  | ETName | ETPattern _ -> NtnInternTypeAny
 
 let set_internalization_type typs =
   List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -954,20 +984,28 @@ let make_internalization_vars recvars mainvars typs =
   maintyps @ extratyps
 
 let make_interpretation_type isrec isonlybinding = function
-  | ETConstr _ ->
-     if isrec then NtnTypeConstrList else
-     if isonlybinding then
-       (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
-       NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
-     else NtnTypeConstr
-  | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
+  (* Parsed as constr list *)
+  | ETConstr (_,None,_) when isrec -> NtnTypeConstrList
+  (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+  | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
+  | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+  (* Parsed as constr, interpreted as constr *)
+  | ETConstr (_,None,_) -> NtnTypeConstr
+  (* Others *)
   | ETName -> NtnTypeBinder NtnParsedAsIdent
   | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
-  | ETBigint | ETReference | ETOther _ -> NtnTypeConstr
+  | ETBigint | ETReference -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
      else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
 
+let subentry_of_constr_prod_entry = function
+  | ETConstr (InCustomEntry s,_,(NumLevel n,_)) -> InCustomEntryLevel (s,n)
+  (* level and use of parentheses for coercion is hard-wired for "constr";
+     we don't remember the level *)
+  | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
+  | _ -> InConstrEntrySomeLevel
+
 let make_interpretation_vars recvars allvars typs =
   let eq_subscope (sc1, l1) (sc2, l2) =
     Option.equal String.equal sc1 sc2 &&
@@ -983,7 +1021,9 @@ let make_interpretation_vars recvars allvars typs =
   let mainvars =
     Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
   Id.Map.mapi (fun x (isonlybinding, sc) ->
-    (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars
+    let typ = Id.List.assoc x typs in
+    ((subentry_of_constr_prod_entry typ,sc),
+     make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1009,17 +1049,42 @@ let warn_non_reversible_notation =
              str " not occur in the right-hand side." ++ spc() ++
              strbrk "The notation will not be used for printing as it is not reversible.")
 
-let is_not_printable onlyparse reversibility = function
-| NVar _ ->
-  if not onlyparse then warn_notation_bound_to_variable ();
-  true
+let make_custom_entry custom level =
+  match custom with
+  | InConstrEntry -> InConstrEntrySomeLevel
+  | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+type entry_coercion_kind =
+  | IsEntryCoercion of notation_entry_level
+  | IsEntryGlobal of string * int
+  | IsEntryIdent of string * int
+
+let is_coercion = function
+  | Some (custom,n,_,[e]) ->
+     (match e, custom with
+     | ETConstr _, _ ->
+         let customkey = make_custom_entry custom n in
+         let subentry = subentry_of_constr_prod_entry e in
+         if notation_entry_level_eq subentry customkey then None
+         else Some (IsEntryCoercion subentry)
+     | ETReference, InCustomEntry s -> Some (IsEntryGlobal (s,n))
+     | ETName, InCustomEntry s -> Some (IsEntryIdent (s,n))
+     | _ -> None)
+  | Some _ -> assert false
+  | None -> None
+
+let printability level onlyparse reversibility = function
+| NVar _ when reversibility = APrioriReversible ->
+  let coe = is_coercion level in
+  if not onlyparse && coe = None then
+    warn_notation_bound_to_variable ();
+  true, coe
 | _ ->
-   if not onlyparse && reversibility <> APrioriReversible then
+   (if not onlyparse && reversibility <> APrioriReversible then
      (warn_non_reversible_notation reversibility; true)
-  else onlyparse
-
+    else onlyparse),None
 
-let find_precedence lev etyps symbols onlyprint =
+let find_precedence custom lev etyps symbols onlyprint =
   let first_symbol =
     let rec aux = function
       | Break _ :: t -> aux t
@@ -1043,10 +1108,9 @@ let find_precedence lev etyps symbols onlyprint =
           else [],Option.get lev
         else
           user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
-      (try match List.assoc x etyps with
-        | ETConstr _ -> test ()
-        | ETConstrAsBinder (_,Some _) -> test ()
-        | (ETName | ETBigint | ETReference) ->
+      (try match List.assoc x etyps, custom with
+        | ETConstr (s,_,Some _), s' when s = s' -> test ()
+        | (ETName | ETBigint | ETReference), _ ->
             begin match lev with
             | None ->
 	      ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1055,7 +1119,7 @@ let find_precedence lev etyps symbols onlyprint =
             | _ ->
               user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
             end
-        | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) ->
+        | (ETPattern _ | ETBinder _ | ETConstr _), _ ->
             (* Give a default ? *)
             if Option.is_empty lev then
               user_err Pp.(str "Need an explicit level.")
@@ -1073,7 +1137,7 @@ let find_precedence lev etyps symbols onlyprint =
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Notgram_ops.level_of_notation "{ _ }" in ()
+  try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
   with Not_found ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1103,7 +1167,7 @@ let remove_curly_brackets l =
 
 module SynData = struct
 
-  type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list
+  type subentry_types = (Id.t * constr_entry_key) list
 
   (* XXX: Document *)
   type syn_data = {
@@ -1137,7 +1201,7 @@ module SynData = struct
 
 end
 
-let find_subentry_types n assoc etyps symbols =
+let find_subentry_types from n assoc etyps symbols =
   let innerlevel = NumLevel 200 in
   let typs =
     find_symbols
@@ -1145,8 +1209,8 @@ let find_subentry_types n assoc etyps symbols =
       (innerlevel,InternalProd)
       (NumLevel n,BorderProd(Right,assoc))
       symbols in
-  let sy_typs = List.map (set_entry_type etyps) typs in
-  let prec = List.map (assoc_of_type n) sy_typs in
+  let sy_typs = List.map (set_entry_type from etyps) typs in
+  let prec = List.map (assoc_of_type from n) sy_typs in
   sy_typs, prec
 
 let compute_syntax_data df modifiers =
@@ -1162,25 +1226,26 @@ let compute_syntax_data df modifiers =
   let _ = check_binder_type recvars mods.etyps in
 
   (* Notations for interp and grammar  *)
-  let ntn_for_interp = make_notation_key symbols in
+  let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
+  let custom = make_custom_entry mods.custom n in
+  let ntn_for_interp = make_notation_key custom symbols in
   let symbols_for_grammar = remove_curly_brackets 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 symbols_for_grammar else ntn_for_interp in
-  if not onlyprint then check_rule_productivity symbols_for_grammar;
-  let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in
+  let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in
+  if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
   (* To globalize... *)
   let etyps = join_auxiliary_recursive_types recvars mods.etyps in
   let sy_typs, prec =
-    find_subentry_types n assoc etyps symbols in
+    find_subentry_types mods.custom n assoc etyps symbols in
   let sy_typs_for_grammar, prec_for_grammar =
     if need_squash then
-      find_subentry_types n assoc etyps symbols_for_grammar
+      find_subentry_types mods.custom n assoc etyps symbols_for_grammar
     else
       sy_typs, prec in
   let i_typs = set_internalization_type sy_typs in
   let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
   let pp_sy_data = (sy_typs,symbols) in
-  let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
+  let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = ntn_for_interp, df' in
 
@@ -1199,7 +1264,7 @@ let compute_syntax_data df modifiers =
     mainvars;
     intern_typs = i_typs;
 
-    level  = (n,prec,List.map snd sy_typs);
+    level  = (mods.custom,n,prec,List.map snd sy_typs);
     pa_syntax_data = pa_sy_data;
     pp_syntax_data = pp_sy_data;
     not_data    = sy_fulldata;
@@ -1222,6 +1287,7 @@ type notation_obj = {
   notobj_local : bool;
   notobj_scope : scope_name option;
   notobj_interp : interpretation;
+  notobj_coercion : entry_coercion_kind option;
   notobj_onlyparse : bool;
   notobj_onlyprint : bool;
   notobj_compat : Flags.compat_version option;
@@ -1243,7 +1309,13 @@ let open_notation i (_, nobj) =
     let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
-      Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat
+      Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
+    (* Declare a possible coercion *)
+    (match nobj.notobj_coercion with
+    | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
+    | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+    | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+    | None -> ())
   end
 
 let cache_notation o =
@@ -1301,7 +1373,7 @@ let recover_notation_syntax ntn =
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =
-  let sq = recover_notation_syntax "{ _ }" in
+  let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
   sy :: sq.synext_notgram.notgram_rules
 
 (**********************************************************************)
@@ -1336,8 +1408,9 @@ let make_pp_rule level (typs,symbols) fmt =
 (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
 let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
   let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
+  let custom,level,_,_ = sd.level in
   let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
-  let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in {
+  let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in {
     synext_level    = sd.level;
     synext_notation = fst sd.info;
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
@@ -1367,13 +1440,14 @@ let add_notation_in_scope local df env c mods scope =
   let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
   let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable sd.only_parsing reversibility ac in
+  let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (** Order is important here! *)
     notobj_onlyparse = onlyparse;
+    notobj_coercion = coe;
     notobj_onlyprint = sd.only_printing;
     notobj_compat = sd.compat;
     notobj_notation = sd.info;
@@ -1387,16 +1461,17 @@ let add_notation_in_scope local df env c mods scope =
 let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
-  let i_typs, onlyprint = if not (is_numeral symbs) then begin
-    let sy = recover_notation_syntax (make_notation_key symbs) in
+  let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
+    let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (** If the only printing flag has been explicitly requested, put it back *)
     let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
-    pi3 sy.synext_level, onlyprint
-  end else [], false in
+    let _,_,_,typs = sy.synext_level in
+    Some sy.synext_level, typs, onlyprint
+  end else None, [], false in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in
-  let df'  = (make_notation_key symbs, (path,df)) in
+  let df'  = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
   let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
   let nenv = {
     ninterp_var_type = to_map i_vars;
@@ -1405,13 +1480,14 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
   let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
   let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable onlyparse reversibility ac in
+  let onlyparse,coe = printability level onlyparse reversibility ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (** Order is important here! *)
     notobj_onlyparse = onlyparse;
+    notobj_coercion = coe;
     notobj_onlyprint = onlyprint;
     notobj_compat = compat;
     notobj_notation = df';
@@ -1462,7 +1538,7 @@ let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
 let add_notation_extra_printing_rule df k v =
   let notk = 
     let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
-    make_notation_key symbs in
+    make_notation_key InConstrEntrySomeLevel symbs in
   add_notation_extra_printing_rule notk k v
 
 (* Infix notations *)
@@ -1546,7 +1622,12 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
       List.map map vars, reversibility, pat
   in
   let onlyparse = match onlyparse with
-    | None when (is_not_printable false reversibility pat) -> Some Flags.Current
+    | None when fst (printability None false reversibility pat) -> Some Flags.Current
     | p -> p
   in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+
+(**********************************************************************)
+(* Declaration of custom entry                                        *)
+
+let declare_custom_entry = Pcoq.create_custom_entries
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index f6de75b079..045b8fa05c 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -60,3 +60,5 @@ val pr_grammar : string -> Pp.t
 val check_infix_modifiers : syntax_modifier list -> unit
 
 val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
+
+val declare_custom_entry : string -> unit
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e5547d9b75..86d6888061 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -97,14 +97,18 @@ open Pputils
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
+  let pr_notation_entry = function
+    | InConstrEntry -> keyword "constr"
+    | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
+
   let pr_at_level = function
     | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
     | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
 
   let pr_constr_as_binder_kind = let open Notation_term in function
-    | AsIdent -> keyword "as ident"
-    | AsIdentOrPattern -> keyword "as pattern"
-    | AsStrictPattern -> keyword "as strict pattern"
+    | AsIdent -> spc () ++ keyword "as ident"
+    | AsIdentOrPattern -> spc () ++ keyword "as pattern"
+    | AsStrictPattern -> spc () ++ keyword "as strict pattern"
 
   let pr_strict b = if b then str "strict " else mt ()
 
@@ -113,9 +117,7 @@ open Pputils
     | ETReference -> str"global"
     | ETPattern (b,None) -> pr_strict b ++ str"pattern"
     | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
-    | ETConstr lev -> str"constr" ++ pr lev
-    | ETOther (_,e) -> str e
-    | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
+    | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
@@ -378,12 +380,11 @@ open Pputils
   let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
 
   let pr_syntax_modifier = function
-    | SetItemLevel (l,n) ->
-      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
-    | SetItemLevelAsBinder (l,bk,n) ->
-      prlist_with_sep sep_v2 str l ++
-      spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
+    | SetItemLevel (l,bko,n) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+      pr_opt pr_constr_as_binder_kind bko
     | 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"
     | SetAssoc RightA -> keyword "right associativity"
     | SetAssoc NonA -> keyword "no associativity"
@@ -674,6 +675,10 @@ open Pputils
         return (
           keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
         )
+      | VernacDeclareCustomEntry s ->
+        return (
+          keyword "Declare Custom Entry " ++ str s
+        )
 
       (* Gallina *)
       | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 653f8b26e0..0f6cbd228e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2096,6 +2096,8 @@ let interp ?proof ~atts ~st c =
       vernac_notation ~atts c infpl sc
   | VernacNotationAddFormat(n,k,v) ->
       Metasyntax.add_notation_extra_printing_rule n k v
+  | VernacDeclareCustomEntry s ->
+      Metasyntax.declare_custom_entry s
 
   (* Gallina *)
   | VernacDefinition ((discharge,kind),lid,d) ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index e97cac818a..8fb74e6d78 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -211,9 +211,9 @@ type proof_expr =
   ident_decl * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
-  | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option
+  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
   | SetLevel of int
+  | SetCustomEntry of string * int option
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing
@@ -333,6 +333,7 @@ type nonrec vernac_expr =
       constr_expr * (lstring * syntax_modifier list) *
       scope_name option
   | VernacNotationAddFormat of string * string * string
+  | VernacDeclareCustomEntry of string
 
   (* Gallina *)
   | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr