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.

13 files changed, 397 insertions, 159 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 ()