Introducing tactic notations in Ltac2.

9 files changed, 533 insertions, 11 deletions

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index 30f5399a88..565be4a199 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -16,11 +16,12 @@ open Misctypes
 open Tac2expr
 open Ltac_plugin
 
-let tac2expr = Gram.entry_create "tactic:tac2expr"
+let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Gram.entry_create "tactic:tac2type"
 let tac2def_val = Gram.entry_create "tactic:tac2def_val"
 let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
 let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
+let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
 let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
@@ -29,7 +30,7 @@ let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
 let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
 
 GEXTEND Gram
-  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext;
+  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
   tac2pat:
     [ "1" LEFTA
       [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
@@ -194,6 +195,30 @@ GEXTEND Gram
         StrPrm (id, t, ml)
     ] ]
   ;
+  syn_node:
+    [ [ "_" -> (!@loc, None)
+      | id = Prim.ident -> (!@loc, Some id)
+    ] ]
+  ;
+  sexpr:
+    [ [ s = Prim.string -> SexprStr (!@loc, s)
+      | n = Prim.integer -> SexprInt (!@loc, n)
+      | id = syn_node -> SexprRec (!@loc, id, [])
+      | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
+        SexprRec (!@loc, id, tok)
+    ] ]
+  ;
+  syn_level:
+    [ [ -> None
+      | ":"; n = Prim.integer -> Some n
+    ] ]
+  ;
+  tac2def_syn:
+    [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
+        e = tac2expr ->
+        StrSyn (toks, n, e)
+    ] ]
+  ;
 END
 
 GEXTEND Gram
@@ -212,6 +237,7 @@ PRINTED BY pr_ltac2entry
 | [ tac2def_val(v) ] -> [ v ]
 | [ tac2def_typ(t) ] -> [ t ]
 | [ tac2def_ext(e) ] -> [ e ]
+| [ tac2def_syn(e) ] -> [ e ]
 END
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF
@@ -250,3 +276,4 @@ open Stdarg
 VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
 | [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ]
 END
+
diff --git a/tac2core.ml b/tac2core.ml
index 3232fcba5b..ad238e6b8f 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -48,10 +48,14 @@ let t_unit = coq_core "unit"
 let t_list = coq_core "list"
 let t_constr = coq_core "constr"
 let t_ident = coq_core "ident"
+let t_option = coq_core "option"
 
 let c_nil = coq_core "[]"
 let c_cons = coq_core "::"
 
+let c_none = coq_core "None"
+let c_some = coq_core "Some"
+
 end
 
 open Core
@@ -464,7 +468,6 @@ let interp_constr flags ist (c, _) =
   end
 
 let () =
-  let open Pretyping in
   let interp ist c = interp_constr (constr_flags ()) ist c in
   let obj = {
     ml_type = t_constr;
@@ -473,7 +476,6 @@ let () =
   define_ml_object Stdarg.wit_constr obj
 
 let () =
-  let open Pretyping in
   let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
   let obj = {
     ml_type = t_constr;
@@ -502,3 +504,71 @@ let () =
     (EConstr.of_constr c, sigma)
   in
   Pretyping.register_constr_interp0 wit_ltac2 interp
+
+(** Built-in notation scopes *)
+
+let add_scope s f =
+  Tac2entries.register_scope (Id.of_string s) f
+
+let scope_fail () = CErrors.user_err (str "Invalid parsing token")
+
+let rthunk e =
+  let loc = Tac2intern.loc_of_tacexpr e in
+  let var = [(loc, Anonymous), Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
+  CTacFun (loc, var, e)
+
+let add_generic_scope s entry arg =
+  let parse = function
+  | [] ->
+    let scope = Extend.Aentry entry in
+    let act x = rthunk (CTacExt (Loc.ghost, in_gen (rawwit arg) x)) in
+    Tac2entries.ScopeRule (scope, act)
+  | _ -> scope_fail ()
+  in
+  add_scope s parse
+
+let () = add_scope "list0" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Alist0 scope in
+  let act l =
+    let l = List.map act l in
+    CTacLst (Loc.ghost, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let sep = Extend.Atoken (CLexer.terminal str) in
+  let scope = Extend.Alist0sep (scope, sep) in
+  let act l =
+    let l = List.map act l in
+    CTacLst (Loc.ghost, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "opt" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Aopt scope in
+  let act opt = match opt with
+  | None ->
+    CTacRef (AbsKn (TacConstructor Core.c_none))
+  | Some x ->
+    CTacApp (Loc.ghost, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "self" begin function
+| [] ->
+  let scope = Extend.Aself in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident
+let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
diff --git a/tac2entries.ml b/tac2entries.ml
index 374a367188..fbfc687ee7 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -19,6 +19,13 @@ open Tac2print
 open Tac2intern
 open Vernacexpr
 
+(** Grammar entries *)
+
+module Pltac =
+struct
+let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
+end
+
 (** Tactic definition *)
 
 type tacdef = {
@@ -98,8 +105,6 @@ let next i =
   let () = incr i in
   ans
 
-let dummy_var i = Id.of_string (Printf.sprintf "_%i" i)
-
 let define_typedef kn (params, def as qdef) = match def with
 | GTydDef _ ->
   Tac2env.define_type kn qdef
@@ -435,10 +440,147 @@ let register_type ?local isrec types = match types with
   let types = List.map map types in
   register_typedef ?local isrec types
 
+(** Parsing *)
+
+type 'a token =
+| TacTerm of string
+| TacNonTerm of Name.t * 'a
+
+type scope_rule =
+| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+
+type scope_interpretation = sexpr list -> scope_rule
+
+let scope_table : scope_interpretation Id.Map.t ref = ref Id.Map.empty
+
+let register_scope id s =
+  scope_table := Id.Map.add id s !scope_table
+
+module ParseToken =
+struct
+
+let loc_of_token = function
+| SexprStr (loc, _) -> loc
+| SexprInt (loc, _) -> loc
+| SexprRec (loc, _, _) -> loc
+
+let parse_scope = function
+| SexprRec (_, (loc, Some id), toks) ->
+  if Id.Map.mem id !scope_table then
+    Id.Map.find id !scope_table toks
+  else
+    CErrors.user_err ~loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
+| tok ->
+  let loc = loc_of_token tok in
+  CErrors.user_err ~loc (str "Invalid parsing token")
+
+let parse_token = function
+| SexprStr (_, s) -> TacTerm s
+| SexprRec (_, (_, na), [tok]) ->
+  let na = match na with None -> Anonymous | Some id -> Name id in
+  let scope = parse_scope tok in
+  TacNonTerm (na, scope)
+| tok ->
+  let loc = loc_of_token tok in
+  CErrors.user_err ~loc (str "Invalid parsing token")
+
+end
+
+let parse_scope = ParseToken.parse_scope
+
+type synext = {
+  synext_tok : sexpr list;
+  synext_exp : raw_tacexpr;
+  synext_lev : int option;
+  synext_loc : bool;
+}
+
+type krule =
+| KRule :
+  (raw_tacexpr, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+  ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
+
+let rec get_rule (tok : scope_rule token list) : krule = match tok with
+| [] -> KRule (Extend.Stop, fun k loc -> k loc [])
+| TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
+  let KRule (rule, act) = get_rule tok in
+  let rule = Extend.Next (rule, scope) in
+  let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
+  KRule (rule, act)
+| TacTerm t :: tok ->
+  let KRule (rule, act) = get_rule tok in
+  let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in
+  let act k _ = act k in
+  KRule (rule, act)
+
+let perform_notation syn st =
+  let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
+  let KRule (rule, act) = get_rule tok in
+  let mk loc args =
+    let map (na, e) =
+      let loc = loc_of_tacexpr e in
+      ((loc, na), None, e)
+    in
+    let bnd = List.map map args in
+    CTacLet (loc, false, bnd, syn.synext_exp)
+  in
+  let rule = Extend.Rule (rule, act mk) in
+  let lev = match syn.synext_lev with
+  | None -> None
+  | Some lev -> Some (string_of_int lev)
+  in
+  let rule = (lev, None, [rule]) in
+  ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st)
+
+let ltac2_notation =
+  Pcoq.create_grammar_command "ltac2-notation" perform_notation
+
+let cache_synext (_, syn) =
+  Pcoq.extend_grammar_command ltac2_notation syn
+
+let open_synext i (_, syn) =
+  if Int.equal i 1 then Pcoq.extend_grammar_command ltac2_notation syn
+
+let subst_synext (subst, syn) =
+  let e = Tac2intern.subst_rawexpr subst syn.synext_exp in
+  if e == syn.synext_exp then syn else { syn with synext_exp = e }
+
+let classify_synext o =
+  if o.synext_loc then Dispose else Substitute o
+
+let inTac2Notation : synext -> obj =
+  declare_object {(default_object "TAC2-NOTATION") with
+     cache_function  = cache_synext;
+     open_function   = open_synext;
+     subst_function = subst_synext;
+     classify_function = classify_synext}
+
+let register_notation ?(local = false) tkn lev body =
+  (** Check that the tokens make sense *)
+  let entries = List.map ParseToken.parse_token tkn in
+  let fold accu tok = match tok with
+  | TacTerm _ -> accu
+  | TacNonTerm (Name id, _) -> Id.Set.add id accu
+  | TacNonTerm (Anonymous, _) -> accu
+  in
+  let ids = List.fold_left fold Id.Set.empty entries in
+  (** Globalize so that names are absolute *)
+  let body = Tac2intern.globalize ids body in
+  let ext = {
+    synext_tok = tkn;
+    synext_exp = body;
+    synext_lev = lev;
+    synext_loc = local;
+  } in
+  Lib.add_anonymous_leaf (inTac2Notation ext)
+
+(** Toplevel entries *)
+
 let register_struct ?local str = match str with
 | StrVal (isrec, e) -> register_ltac ?local isrec e
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
+| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
 
 (** Printing *)
 
diff --git a/tac2entries.mli b/tac2entries.mli
index 0d9b3ad134..71e8150057 100644
--- a/tac2entries.mli
+++ b/tac2entries.mli
@@ -24,6 +24,22 @@ val register_primitive : ?local:bool ->
 
 val register_struct : ?local:bool -> strexpr -> unit
 
+val register_notation : ?local:bool -> sexpr list -> int option ->
+  raw_tacexpr -> unit
+
+(** {5 Notations} *)
+
+type scope_rule =
+| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+
+type scope_interpretation = sexpr list -> scope_rule
+
+val register_scope : Id.t -> scope_interpretation -> unit
+(** Create a new scope with the provided name *)
+
+val parse_scope : sexpr -> scope_rule
+(** Use this to interpret the subscopes for interpretation functions *)
+
 (** {5 Inspecting} *)
 
 val print_ltac : Libnames.reference -> unit
@@ -32,3 +48,10 @@ val print_ltac : Libnames.reference -> unit
 
 (** Evaluate a tactic expression in the current environment *)
 val call : default:bool -> raw_tacexpr -> unit
+
+(** {5 Parsing entries} *)
+
+module Pltac :
+sig
+val tac2expr : raw_tacexpr Pcoq.Gram.entry
+end
diff --git a/tac2expr.mli b/tac2expr.mli
index 63207ac78f..acdad9bab4 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -129,7 +129,23 @@ type glb_tacexpr =
 | GTacExt of glob_generic_argument
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
-(** Toplevel statements *)
+(** {5 Parsing & Printing} *)
+
+type exp_level =
+| E5
+| E4
+| E3
+| E2
+| E1
+| E0
+
+type sexpr =
+| SexprStr of string located
+| SexprInt of int located
+| SexprRec of Loc.t * Id.t option located * sexpr list
+
+(** {5 Toplevel statements} *)
+
 type strexpr =
 | StrVal of rec_flag * (Name.t located * raw_tacexpr) list
   (** Term definition *)
@@ -137,6 +153,9 @@ type strexpr =
   (** Type definition *)
 | StrPrm of Id.t located * raw_typexpr * ml_tactic_name
   (** External definition *)
+| StrSyn of sexpr list * int option * raw_tacexpr
+  (** Syntactic extensions *)
+
 
 (** {5 Dynamic semantics} *)
 
diff --git a/tac2intern.ml b/tac2intern.ml
index c7e02a7b06..17d08b2285 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -476,10 +476,10 @@ let check_redundant_clause = function
 | [] -> ()
 | (p, _) :: _ -> warn_redundant_clause ~loc:(loc_of_patexpr p) ()
 
-let get_variable env var = match var with
+let get_variable0 mem var = match var with
 | RelId (loc, qid) ->
   let (dp, id) = repr_qualid qid in
-  if DirPath.is_empty dp && Id.Map.mem id env.env_var then ArgVar (loc, id)
+  if DirPath.is_empty dp && mem id then ArgVar (loc, id)
   else
     let kn =
       try Tac2env.locate_ltac qid
@@ -489,6 +489,10 @@ let get_variable env var = match var with
     ArgArg kn
 | AbsKn kn -> ArgArg kn
 
+let get_variable env var =
+  let mem id = Id.Map.mem id env.env_var in
+  get_variable0 mem var
+
 let get_constructor env var = match var with
 | RelId (loc, qid) ->
   let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
@@ -1106,6 +1110,104 @@ let intern_open_type t =
   let t = normalize env (count, vars) t in
   (!count, t)
 
+(** Globalization *)
+
+let add_name accu = function
+| Name id -> Id.Set.add id accu
+| Anonymous -> accu
+
+let get_projection0 var = match var with
+| RelId (loc, qid) ->
+  let kn = try Tac2env.locate_projection qid with Not_found ->
+    user_err ~loc (pr_qualid qid ++ str " is not a projection")
+  in
+  kn
+| AbsKn kn -> kn
+
+let rec globalize ids e = match e with
+| CTacAtm _ -> e
+| CTacRef ref ->
+  let mem id = Id.Set.mem id ids in
+  begin match get_variable0 mem ref with
+  | ArgVar _ -> e
+  | ArgArg kn -> CTacRef (AbsKn kn)
+  end
+| CTacFun (loc, bnd, e) ->
+  let fold accu ((_, na), _) = add_name accu na in
+  let ids = List.fold_left fold ids bnd in
+  let e = globalize ids e in
+  CTacFun (loc, bnd, e)
+| CTacApp (loc, e, el) ->
+  let e = globalize ids e in
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacApp (loc, e, el)
+| CTacLet (loc, isrec, bnd, e) ->
+  let fold accu ((_, na), _, _) = add_name accu na in
+  let ext = List.fold_left fold Id.Set.empty bnd in
+  let eids = Id.Set.union ext ids in
+  let e = globalize eids e in
+  let map (qid, t, e) =
+    let ids = if isrec then eids else ids in
+    (qid, t, globalize ids e)
+  in
+  let bnd = List.map map bnd in
+  CTacLet (loc, isrec, bnd, e)
+| CTacTup (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacTup (loc, el)
+| CTacArr (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacArr (loc, el)
+| CTacLst (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacLst (loc, el)
+| CTacCnv (loc, e, t) ->
+  let e = globalize ids e in
+  CTacCnv (loc, e, t)
+| CTacSeq (loc, e1, e2) ->
+  let e1 = globalize ids e1 in
+  let e2 = globalize ids e2 in
+  CTacSeq (loc, e1, e2)
+| CTacCse (loc, e, bl) ->
+  let e = globalize ids e in
+  let bl = List.map (fun b -> globalize_case ids b) bl in
+  CTacCse (loc, e, bl)
+| CTacRec (loc, r) ->
+  let map (p, e) =
+    let p = get_projection0 p in
+    let e = globalize ids e in
+    (AbsKn p, e)
+  in
+  CTacRec (loc, List.map map r)
+| CTacPrj (loc, e, p) ->
+  let e = globalize ids e in
+  let p = get_projection0 p in
+  CTacPrj (loc, e, AbsKn p)
+| CTacSet (loc, e, p, e') ->
+  let e = globalize ids e in
+  let p = get_projection0 p in
+  let e' = globalize ids e' in
+  CTacSet (loc, e, AbsKn p, e')
+| CTacExt (loc, arg) ->
+  let arg = pr_argument_type (genarg_tag arg) in
+  CErrors.user_err ~loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
+
+and globalize_case ids (p, e) =
+  (globalize_pattern ids p, globalize ids e)
+
+and globalize_pattern ids p = match p with
+| CPatAny _ -> p
+| CPatRef (loc, cst, pl) ->
+  let cst = match get_constructor () cst with
+  | ArgVar _ -> cst
+  | ArgArg (_, knc) -> AbsKn knc
+  in
+  let pl = List.map (fun p -> globalize_pattern ids p) pl in
+  CPatRef (loc, cst, pl)
+| CPatTup (loc, pl) ->
+  let pl = List.map (fun p -> globalize_pattern ids p) pl in
+  CPatTup (loc, pl)
+
 (** Kernel substitution *)
 
 open Mod_subst
@@ -1213,6 +1315,128 @@ let subst_type_scheme subst (prm, t as sch) =
   let t' = subst_type subst t in
   if t' == t then sch else (prm, t')
 
+let subst_or_relid subst ref = match ref with
+| RelId _ -> ref
+| AbsKn kn ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn kn'
+
+let rec subst_rawtype subst t = match t with
+| CTypVar _ -> t
+| CTypArrow (loc, t1, t2) ->
+  let t1' = subst_rawtype subst t1 in
+  let t2' = subst_rawtype subst t2 in
+  if t1' == t1 && t2' == t2 then t else CTypArrow (loc, t1', t2')
+| CTypTuple (loc, tl) ->
+  let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
+  if tl' == tl then t else CTypTuple (loc, tl')
+| CTypRef (loc, ref, tl) ->
+  let ref' = subst_or_relid subst ref in
+  let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
+  if ref' == ref && tl' == tl then t else CTypRef (loc, ref', tl')
+
+let subst_tacref subst ref = match ref with
+| RelId _ -> ref
+| AbsKn (TacConstant kn) ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn (TacConstant kn')
+| AbsKn (TacConstructor kn) ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn (TacConstructor kn')
+
+let subst_projection subst prj = match prj with
+| RelId _ -> prj
+| AbsKn kn ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then prj else AbsKn kn'
+
+let rec subst_rawpattern subst p = match p with
+| CPatAny _ -> p
+| CPatRef (loc, c, pl) ->
+  let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
+  let c' = match c with
+  | RelId _ -> c
+  | AbsKn kn ->
+    let kn' = subst_kn subst kn in
+    if kn' == kn then c else AbsKn kn'
+  in
+  if pl' == pl && c' == c then p else CPatRef (loc, c', pl')
+| CPatTup (loc, pl) ->
+  let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
+  if pl' == pl then p else CPatTup (loc, pl')
+
+(** Used for notations *)
+let rec subst_rawexpr subst t = match t with
+| CTacAtm _ -> t
+| CTacRef ref ->
+  let ref' = subst_tacref subst ref in
+  if ref' == ref then t else CTacRef ref'
+| CTacFun (loc, bnd, e) ->
+  let map (na, t as p) =
+    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
+    if t' == t then p else (na, t')
+  in
+  let bnd' = List.smartmap map bnd in
+  let e' = subst_rawexpr subst e in
+  if bnd' == bnd && e' == e then t else CTacFun (loc, bnd', e')
+| CTacApp (loc, e, el) ->
+  let e' = subst_rawexpr subst e in
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if e' == e && el' == el then t else CTacApp (loc, e', el')
+| CTacLet (loc, isrec, bnd, e) ->
+  let map (na, t, e as p) =
+    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
+    let e' = subst_rawexpr subst e in
+    if t' == t && e' == e then p else (na, t', e')
+  in
+  let bnd' = List.smartmap map bnd in
+  let e' = subst_rawexpr subst e in
+  if bnd' == bnd && e' == e then t else CTacLet (loc, isrec, bnd', e')
+| CTacTup (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacTup (loc, el')
+| CTacArr (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacArr (loc, el')
+| CTacLst (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacLst (loc, el')
+| CTacCnv (loc, e, c) ->
+  let e' = subst_rawexpr subst e in
+  let c' = subst_rawtype subst c in
+  if c' == c && e' == e then t else CTacCnv (loc, e', c')
+| CTacSeq (loc, e1, e2) ->
+  let e1' = subst_rawexpr subst e1 in
+  let e2' = subst_rawexpr subst e2 in
+  if e1' == e1 && e2' == e2 then t else CTacSeq (loc, e1', e2')
+| CTacCse (loc, e, bl) ->
+  let map (p, e as x) =
+    let p' = subst_rawpattern subst p in
+    let e' = subst_rawexpr subst e in
+    if p' == p && e' == e then x else (p', e')
+  in
+  let e' = subst_rawexpr subst e in
+  let bl' = List.smartmap map bl in
+  if e' == e && bl' == bl then t else CTacCse (loc, e', bl')
+| CTacRec (loc, el) ->
+  let map (prj, e as p) =
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    if prj' == prj && e' == e then p else (prj', e')
+  in
+  let el' = List.smartmap map el in
+  if el' == el then t else CTacRec (loc, el')
+| CTacPrj (loc, e, prj) ->
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    if prj' == prj && e' == e then t else CTacPrj (loc, e', prj')
+| CTacSet (loc, e, prj, r) ->
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    let r' = subst_rawexpr subst r in
+    if prj' == prj && e' == e && r' == r then t else CTacSet (loc, e', prj', r')
+| CTacExt _ -> assert false (** Should not be generated by gloabalization *)
+
 (** Registering *)
 
 let () =
diff --git a/tac2intern.mli b/tac2intern.mli
index 4c482d0b0c..3d400a5cdd 100644
--- a/tac2intern.mli
+++ b/tac2intern.mli
@@ -27,6 +27,14 @@ val subst_expr : substitution -> glb_tacexpr -> glb_tacexpr
 val subst_quant_typedef : substitution -> glb_quant_typedef -> glb_quant_typedef
 val subst_type_scheme : substitution -> type_scheme -> type_scheme
 
+val subst_rawexpr : substitution -> raw_tacexpr -> raw_tacexpr
+
+(** {5 Notations} *)
+
+val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
+(** Replaces all qualified identifiers by their corresponding kernel name. The
+    set represents bound variables in the context. *)
+
 (** Errors *)
 
 val error_nargs_mismatch : Loc.t -> int -> int -> 'a
diff --git a/tac2print.ml b/tac2print.ml
index ffa5ddc05a..e6f0582e3d 100644
--- a/tac2print.ml
+++ b/tac2print.ml
@@ -33,7 +33,7 @@ type typ_level =
 let pr_typref kn =
   Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
 
-let rec pr_glbtype_gen pr lvl c =
+let pr_glbtype_gen pr lvl c =
   let rec pr_glbtype lvl = function
   | GTypVar n -> str "'" ++ str (pr n)
   | GTypRef (kn, []) -> pr_typref kn
@@ -88,7 +88,7 @@ let pr_constructor kn =
 let pr_projection kn =
   Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn)
 
-type exp_level =
+type exp_level = Tac2expr.exp_level =
 | E5
 | E4
 | E3
diff --git a/tac2print.mli b/tac2print.mli
index 94555a4c95..ddd599641d 100644
--- a/tac2print.mli
+++ b/tac2print.mli
@@ -12,13 +12,22 @@ open Tac2expr
 
 (** {5 Printing types} *)
 
+type typ_level =
+| T5_l
+| T5_r
+| T2
+| T1
+| T0
+
 val pr_typref : type_constant -> std_ppcmds
+val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> std_ppcmds
 val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> std_ppcmds
 
 (** {5 Printing expressions} *)
 
 val pr_constructor : ltac_constructor -> std_ppcmds
 val pr_projection : ltac_projection -> std_ppcmds
+val pr_glbexpr_gen : exp_level -> glb_tacexpr -> std_ppcmds
 val pr_glbexpr : glb_tacexpr -> std_ppcmds
 
 (** {5 Utilities} *)