Towards a proper printing of Ltac2 data structures.

11 files changed, 401 insertions, 38 deletions

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index 1dbd223b22..9384584f19 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -56,7 +56,7 @@ GEXTEND Gram
       [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
       | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, qid)
       | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, qid, r)
-      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "0" SEP "," -> CTacTup (!@loc, e0 :: el) ]
+      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (!@loc, e0 :: el) ]
     | "0"
       [ "("; a = tac2expr LEVEL "5"; ")" -> a
       | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
diff --git a/ltac2_plugin.mlpack b/ltac2_plugin.mlpack
index 561bd0eb0a..3d87a8cddb 100644
--- a/ltac2_plugin.mlpack
+++ b/ltac2_plugin.mlpack
@@ -1,4 +1,5 @@
 Tac2env
+Tac2print
 Tac2intern
 Tac2interp
 Tac2entries
diff --git a/tac2entries.ml b/tac2entries.ml
index 93ad0ceb0b..f4b3147c48 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -15,6 +15,7 @@ open Libobject
 open Nametab
 open Tac2env
 open Tac2expr
+open Tac2print
 open Tac2intern
 open Vernacexpr
 
@@ -303,11 +304,17 @@ let print_ltac ref =
   in
   match kn with
   | TacConstant kn ->
-    let (_, (_, t)) = Tac2env.interp_global kn in
-    Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t)
+    let (e, _, (_, t)) = Tac2env.interp_global kn in
+    let name = int_name () in
+    Feedback.msg_notice (
+      hov 0 (
+        hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ fnl () ++
+        hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
+      )
+    )
   | TacConstructor kn ->
     let _ = Tac2env.interp_constructor kn in
-    Feedback.msg_notice (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid)
+    Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
 
 (** Calling tactics *)
 
diff --git a/tac2env.ml b/tac2env.ml
index a058d764e7..18519a6ce1 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -73,7 +73,7 @@ let define_global kn e =
 
 let interp_global kn =
   let (e, t) = KNmap.find kn ltac_state.contents.ltac_tactics in
-  (eval_pure e, t)
+  (e, eval_pure e, t)
 
 let define_constructor kn t =
   let state = !ltac_state in
@@ -139,21 +139,33 @@ module RfTab = Nametab.Make(FullPath)(TacRef)
 
 type nametab = {
   tab_ltac : RfTab.t;
+  tab_ltac_rev : full_path KNmap.t * full_path KNmap.t;
   tab_type : KnTab.t;
+  tab_type_rev : full_path KNmap.t;
   tab_proj : KnTab.t;
+  tab_proj_rev : full_path KNmap.t;
 }
 
 let empty_nametab = {
   tab_ltac = RfTab.empty;
+  tab_ltac_rev = (KNmap.empty, KNmap.empty);
   tab_type = KnTab.empty;
+  tab_type_rev = KNmap.empty;
   tab_proj = KnTab.empty;
+  tab_proj_rev = KNmap.empty;
 }
 
 let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
 
 let push_ltac vis sp kn =
   let tab = !nametab in
-  nametab := { tab with tab_ltac = RfTab.push vis sp kn tab.tab_ltac }
+  let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
+  let (constant_map, constructor_map) = tab.tab_ltac_rev in
+  let tab_ltac_rev = match kn with
+  | TacConstant c -> (KNmap.add c sp constant_map, constructor_map)
+  | TacConstructor c -> (constant_map, KNmap.add c sp constructor_map)
+  in
+  nametab := { tab with tab_ltac; tab_ltac_rev }
 
 let locate_ltac qid =
   let tab = !nametab in
@@ -163,9 +175,19 @@ let locate_extended_all_ltac qid =
   let tab = !nametab in
   RfTab.find_prefixes qid tab.tab_ltac
 
+let shortest_qualid_of_ltac kn =
+  let tab = !nametab in
+  let sp = match kn with
+  | TacConstant c -> KNmap.find c (fst tab.tab_ltac_rev)
+  | TacConstructor c -> KNmap.find c (snd tab.tab_ltac_rev)
+  in
+  RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+
 let push_type vis sp kn =
   let tab = !nametab in
-  nametab := { tab with tab_type = KnTab.push vis sp kn tab.tab_type }
+  let tab_type = KnTab.push vis sp kn tab.tab_type in
+  let tab_type_rev = KNmap.add kn sp tab.tab_type_rev in
+  nametab := { tab with tab_type; tab_type_rev }
 
 let locate_type qid =
   let tab = !nametab in
@@ -175,9 +197,16 @@ let locate_extended_all_type qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_type
 
+let shortest_qualid_of_type kn =
+  let tab = !nametab in
+  let sp = KNmap.find kn tab.tab_type_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_type
+
 let push_projection vis sp kn =
   let tab = !nametab in
-  nametab := { tab with tab_proj = KnTab.push vis sp kn tab.tab_proj }
+  let tab_proj = KnTab.push vis sp kn tab.tab_proj in
+  let tab_proj_rev = KNmap.add kn sp tab.tab_proj_rev in
+  nametab := { tab with tab_proj; tab_proj_rev }
 
 let locate_projection qid =
   let tab = !nametab in
@@ -187,6 +216,11 @@ let locate_extended_all_projection qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_proj
 
+let shortest_qualid_of_projection kn =
+  let tab = !nametab in
+  let sp = KNmap.find kn tab.tab_proj_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
+
 type 'a ml_object = {
   ml_type : type_constant;
   ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
diff --git a/tac2env.mli b/tac2env.mli
index 4d2a1645ea..16232ec810 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -17,7 +17,7 @@ open Tac2expr
 (** {5 Toplevel definition of values} *)
 
 val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
-val interp_global : ltac_constant -> (valexpr * type_scheme)
+val interp_global : ltac_constant -> (glb_tacexpr * valexpr * type_scheme)
 
 (** {5 Toplevel definition of types} *)
 
@@ -69,14 +69,17 @@ type tacref =
 val push_ltac : visibility -> full_path -> tacref -> unit
 val locate_ltac : qualid -> tacref
 val locate_extended_all_ltac : qualid -> tacref list
+val shortest_qualid_of_ltac : tacref -> qualid
 
 val push_type : visibility -> full_path -> type_constant -> unit
 val locate_type : qualid -> type_constant
 val locate_extended_all_type : qualid -> type_constant list
+val shortest_qualid_of_type : type_constant -> qualid
 
 val push_projection : visibility -> full_path -> ltac_projection -> unit
 val locate_projection : qualid -> ltac_projection
 val locate_extended_all_projection : qualid -> ltac_projection list
+val shortest_qualid_of_projection : ltac_projection -> qualid
 
 (** {5 Toplevel definitions of ML tactics} *)
 
diff --git a/tac2expr.mli b/tac2expr.mli
index c3c1e56dea..7a2c684fbc 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -105,8 +105,8 @@ type glb_tacexpr =
 | GTacArr of glb_tacexpr list
 | GTacCst of type_constant * int * glb_tacexpr list
 | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
-| GTacPrj of glb_tacexpr * int
-| GTacSet of glb_tacexpr * int * glb_tacexpr
+| GTacPrj of type_constant * glb_tacexpr * int
+| GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
 | GTacExt of glob_generic_argument
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
diff --git a/tac2intern.ml b/tac2intern.ml
index bc15b567d4..350dc4efe6 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -14,6 +14,7 @@ open Names
 open Libnames
 open Misctypes
 open Tac2env
+open Tac2print
 open Tac2expr
 
 (** Hardwired types and constants *)
@@ -50,6 +51,7 @@ sig
   val add : key -> 'a -> 'a t -> 'a t
   val mem : key -> 'a t -> bool
   val find : key -> 'a t -> 'a
+  val exists : (key -> 'a -> bool) -> 'a t -> bool
 end
 end
 =
@@ -143,6 +145,31 @@ let empty_env () = {
   env_rec = Id.Map.empty;
 }
 
+let env_name env =
+  (** Generate names according to a provided environment *)
+  let mk num =
+    let base = num mod 26 in
+    let rem = num / 26 in
+    let name = String.make 1 (Char.chr (97 + base)) in
+    let suff = if Int.equal rem 0 then "" else string_of_int rem in
+    let name = name ^ suff in
+    name
+  in
+  let fold id elt acc = UF.Map.add elt (Id.to_string id) acc in
+  let vars = Id.Map.fold fold env.env_als.contents UF.Map.empty in
+  let vars = ref vars in
+  let rec fresh n =
+    let name = mk n in
+    if UF.Map.exists (fun _ name' -> String.equal name name') !vars then fresh (succ n)
+    else name
+  in
+  fun n ->
+    if UF.Map.mem n !vars then UF.Map.find n !vars
+    else
+      let ans = fresh 0 in
+      let () = vars := UF.Map.add n ans !vars in
+      ans
+
 let ltac2_env : environment Genintern.Store.field =
   Genintern.Store.field ()
 
@@ -311,19 +338,12 @@ let rec unify env t1 t2 = match kind env t1, kind env t2 with
   else raise (CannotUnify (t1, t2))
 | _ -> raise (CannotUnify (t1, t2))
 
-(** FIXME *)
-let rec pr_glbtype = function
-| GTypVar n -> str "?"
-| GTypRef (kn, tl) ->
-  KerName.print kn ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")"
-| GTypArrow (t1, t2) -> str "Arr(" ++ pr_glbtype t1 ++ str ", " ++ pr_glbtype t2 ++ str ")"
-| GTypTuple tl -> str "Tup(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")"
-
 let unify loc env t1 t2 =
   try unify env t1 t2
   with CannotUnify (u1, u2) ->
-    user_err ~loc (str "This expression has type " ++ pr_glbtype t1 ++
-      str " but an expression what expected of type " ++ pr_glbtype t2)
+    let name = env_name env in
+    user_err ~loc (str "This expression has type " ++ pr_glbtype name t1 ++
+      str " but an expression what expected of type " ++ pr_glbtype name t2)
 
 (** Term typing *)
 
@@ -418,13 +438,15 @@ let check_elt_empty loc env t = match kind env t with
 | GTypVar _ ->
   user_err ~loc (str "Cannot infer an empty type for this expression")
 | GTypArrow _ | GTypTuple _ ->
-  user_err ~loc (str "Type " ++ pr_glbtype t ++ str " is not an empty type")
+  let name = env_name env in
+  user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type")
 | GTypRef (kn, _) ->
   let def = Tac2env.interp_type kn in
   match def with
   | _, GTydAlg [] -> kn
   | _ ->
-    user_err ~loc (str "Type " ++ pr_glbtype t ++ str " is not an empty type")
+    let name = env_name env in
+    user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type")
 
 let check_unit ?loc t =
   let maybe_unit = match t with
@@ -475,11 +497,11 @@ let intern_atm env = function
 
 let invalid_pattern ~loc kn t =
   let pt = match t with
-  | GCaseAlg kn' -> KerName.print kn
+  | GCaseAlg kn' -> pr_typref kn
   | GCaseTuple n -> str "tuple"
   in
   user_err ~loc (str "Invalid pattern, expected a pattern for type " ++
-    KerName.print kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
+    pr_typref kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
 
 type pattern_kind =
 | PKind_empty
@@ -527,7 +549,7 @@ let rec intern_rec env = function
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
-    let (_, sch) = Tac2env.interp_global kn in
+    let (_, _, sch) = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
   | ArgArg (TacConstructor kn) ->
     intern_constructor env (fst qid) kn []
@@ -542,6 +564,7 @@ let rec intern_rec env = function
     (env, na :: bnd, t :: tl)
   in
   let (env, bnd, tl) = List.fold_left fold (env, [], []) bnd in
+  let bnd = List.rev bnd in
   let (e, t) = intern_rec env e in
   let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
   (GTacFun (bnd, e), t)
@@ -637,7 +660,7 @@ let rec intern_rec env = function
   let () = unify loc env t exp in
   let substf i = GTypVar subst.(i) in
   let ret = subst_type substf pinfo.pdata_ptyp in
-  (GTacPrj (e, pinfo.pdata_indx), ret)
+  (GTacPrj (pinfo.pdata_type, e, pinfo.pdata_indx), ret)
 | CTacSet (loc, e, proj, r) ->
   let pinfo = get_projection proj in
   let () =
@@ -652,7 +675,7 @@ let rec intern_rec env = function
   let substf i = GTypVar subst.(i) in
   let ret = subst_type substf pinfo.pdata_ptyp in
   let r = intern_rec_with_constraint env r ret in
-  (GTacSet (e, pinfo.pdata_indx, r), GTypRef (t_unit, []))
+  (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (t_unit, []))
 | CTacExt (loc, ext) ->
   let open Genintern in
   let GenArg (Rawwit tag, _) = ext in
@@ -899,7 +922,7 @@ and intern_record env loc fs =
           several times")
     else
       user_err ~loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
-        pertain to record definition " ++ KerName.print pinfo.pdata_type)
+        pertain to record definition " ++ pr_typref pinfo.pdata_type)
   in
   let () = List.iter iter fs in
   let () = match Array.findi (fun _ o -> Option.is_empty o) args with
@@ -1017,13 +1040,15 @@ let rec subst_expr subst e = match e with
   let cse1' = Array.map (fun (ids, e) -> (ids, subst_expr subst e)) cse1 in
   let ci' = subst_case_info subst ci in
   GTacCse (subst_expr subst e, ci', cse0', cse1')
-| GTacPrj (e, p) as e0 ->
+| GTacPrj (kn, e, p) as e0 ->
+  let kn' = subst_kn subst kn in
   let e' = subst_expr subst e in
-  if e' == e then e0 else GTacPrj (e', p)
-| GTacSet (e, p, r) as e0 ->
+  if kn' == kn && e' == e then e0 else GTacPrj (kn', e', p)
+| GTacSet (kn, e, p, r) as e0 ->
+  let kn' = subst_kn subst kn in
   let e' = subst_expr subst e in
   let r' = subst_expr subst r in
-  if e' == e && r' == r then e0 else GTacSet (e', p, r')
+  if kn' == kn && e' == e && r' == r then e0 else GTacSet (kn', e', p, r')
 | GTacExt ext ->
   let ext' = Genintern.generic_substitute subst ext in
   if ext' == ext then e else GTacExt ext'
diff --git a/tac2intern.mli b/tac2intern.mli
index a6be01d647..6633792e7e 100644
--- a/tac2intern.mli
+++ b/tac2intern.mli
@@ -26,5 +26,3 @@ val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr
 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 pr_glbtype : 'a glb_typexpr -> Pp.std_ppcmds
diff --git a/tac2interp.ml b/tac2interp.ml
index d508b0c967..f93c8cb5fe 100644
--- a/tac2interp.ml
+++ b/tac2interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open CErrors
 open Genarg
@@ -30,7 +31,7 @@ let get_var ist id =
     anomaly (str "Unbound variable " ++ Id.print id)
 
 let get_ref ist kn =
-  try fst (Tac2env.interp_global kn) with Not_found ->
+  try pi2 (Tac2env.interp_global kn) with Not_found ->
     anomaly (str "Unbound reference" ++ KerName.print kn)
 
 let return = Proofview.tclUNIT
@@ -82,9 +83,9 @@ let rec interp ist = function
   return (ValBlk (n, Array.of_list el))
 | GTacCse (e, _, cse0, cse1) ->
   interp ist e >>= fun e -> interp_case ist e cse0 cse1
-| GTacPrj (e, p) ->
+| GTacPrj (_, e, p) ->
   interp ist e >>= fun e -> interp_proj ist e p
-| GTacSet (e, p, r) ->
+| GTacSet (_, e, p, r) ->
   interp ist e >>= fun e ->
   interp ist r >>= fun r ->
   interp_set ist e p r
diff --git a/tac2print.ml b/tac2print.ml
new file mode 100644
index 0000000000..96d0ceb875
--- /dev/null
+++ b/tac2print.ml
@@ -0,0 +1,266 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Pp
+open Genarg
+open Names
+open Tac2expr
+open Tac2env
+
+(** Utils *)
+
+let change_kn_label kn id =
+  let (mp, dp, _) = KerName.repr kn in
+  KerName.make mp dp (Label.of_id id)
+
+let paren p = hov 2 (str "(" ++ p ++ str ")")
+
+(** Type printing *)
+
+type typ_level =
+| T5_l
+| T5_r
+| T2
+| T1
+| T0
+
+let pr_typref kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
+
+let rec pr_glbtype_gen pr lvl c =
+  let rec pr_glbtype lvl = function
+  | GTypVar n -> str "'" ++ str (pr n)
+  | GTypRef (kn, []) -> pr_typref kn
+  | GTypRef (kn, [t]) ->
+    let paren = match lvl with
+    | T5_r | T5_l | T2 | T1 -> fun x -> x
+    | T0 -> paren
+    in
+    paren (pr_glbtype lvl t ++ spc () ++ pr_typref kn)
+  | GTypRef (kn, tl) ->
+    let paren = match lvl with
+    | T5_r | T5_l | T2 | T1 -> fun x -> x
+    | T0 -> paren
+    in
+    paren (str "(" ++ prlist_with_sep (fun () -> str ", ") (pr_glbtype lvl) tl ++ str ")" ++ spc () ++ pr_typref kn)
+  | GTypArrow (t1, t2) ->
+    let paren = match lvl with
+    | T5_r -> fun x -> x
+    | T5_l | T2 | T1 | T0 -> paren
+    in
+    paren (pr_glbtype T5_l t1 ++ spc () ++ str "->" ++ spc () ++ pr_glbtype T5_r t2)
+  | GTypTuple tl ->
+    let paren = match lvl with
+    | T5_r | T5_l -> fun x -> x
+    | T2 | T1 | T0 -> paren
+    in
+    paren (prlist_with_sep (fun () -> str " * ") (pr_glbtype T2) tl)
+  in
+  hov 0 (pr_glbtype lvl c)
+
+let pr_glbtype pr c = pr_glbtype_gen pr T5_r c
+
+let int_name () =
+  let vars = ref Int.Map.empty in
+  fun n ->
+    if Int.Map.mem n !vars then Int.Map.find n !vars
+    else
+      let num = Int.Map.cardinal !vars in
+      let base = num mod 26 in
+      let rem = num / 26 in
+      let name = String.make 1 (Char.chr (97 + base)) in
+      let suff = if Int.equal rem 0 then "" else string_of_int rem in
+      let name = name ^ suff in
+      let () = vars := Int.Map.add n name !vars in
+      name
+
+(** Term printing *)
+
+let pr_constructor kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstructor kn))
+
+let pr_projection kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn)
+
+type exp_level =
+| E5
+| E4
+| E3
+| E2
+| E1
+| E0
+
+let pr_atom = function
+| AtmInt n -> int n
+| AtmStr s -> qstring s
+
+let pr_name = function
+| Name id -> Id.print id
+| Anonymous -> str "_"
+
+let find_constructor n empty def =
+  let rec find n = function
+  | [] -> assert false
+  | (id, []) :: rem ->
+    if empty then
+      if Int.equal n 0 then id
+      else find (pred n) rem
+    else find n rem
+  | (id, _ :: _) :: rem ->
+    if not empty then
+      if Int.equal n 0 then id
+      else find (pred n) rem
+    else find n rem
+  in
+  find n def
+
+let order_branches cbr nbr def =
+  let rec order cidx nidx def = match def with
+  | [] -> []
+  | (id, []) :: rem ->
+    let ans = order (succ cidx) nidx rem in
+    (id, [], cbr.(cidx)) :: ans
+  | (id, _ :: _) :: rem ->
+    let ans = order cidx (succ nidx) rem in
+    let (vars, e) = nbr.(nidx) in
+    (id, Array.to_list vars, e) :: ans
+  in
+  order 0 0 def
+
+let pr_glbexpr_gen lvl c =
+  let rec pr_glbexpr lvl = function
+  | GTacAtm atm -> pr_atom atm
+  | GTacVar id -> Id.print id
+  | GTacRef gr ->
+    let qid = shortest_qualid_of_ltac (TacConstant gr) in
+    Libnames.pr_qualid qid
+  | GTacFun (nas, c) ->
+    let nas = pr_sequence pr_name nas in
+    let paren = match lvl with
+    | E0 | E1 | E2 | E3 | E4 -> paren
+    | E5 -> fun x -> x
+    in
+    paren (str "fun" ++ spc () ++ nas ++ spc () ++ str "=>" ++ spc () ++
+      hov 0 (pr_glbexpr E5 c))
+  | GTacApp (c, cl) ->
+    let paren = match lvl with
+    | E0 -> paren
+    | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    paren (pr_glbexpr E1 c) ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)
+  | GTacLet (mut, bnd, e) ->
+    let paren = match lvl with
+    | E0 | E1 | E2 | E3 | E4 -> paren
+    | E5 -> fun x -> x
+    in
+    let mut = if mut then str "rec" ++ spc () else mt () in
+    let pr_bnd (na, e) =
+      pr_name na ++ spc () ++ str ":=" ++ spc () ++ hov 2 (pr_glbexpr E5 e) ++ spc ()
+    in
+    let bnd = prlist_with_sep (fun () -> str "with" ++ spc ()) pr_bnd bnd in
+    paren (str "let" ++ spc () ++ mut ++ bnd ++ str "in" ++ spc () ++ pr_glbexpr E5 e)
+  | GTacTup cl ->
+    let paren = match lvl with
+    | E0 | E1 -> paren
+    | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    paren (prlist_with_sep (fun () -> str "," ++ spc ()) (pr_glbexpr E1) cl)
+  | GTacArr cl ->
+    mt () (** FIXME when implemented *)
+  | GTacCst (tpe, n, cl) ->
+    begin match Tac2env.interp_type tpe with
+    | _, GTydAlg def ->
+      let paren = match lvl with
+      | E0 -> paren
+      | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+      in
+      let id = find_constructor n (List.is_empty cl) def in
+      let kn = change_kn_label tpe id in
+      let cl = match cl with
+      | [] -> mt ()
+      | _ -> spc () ++ pr_sequence (pr_glbexpr E0) cl
+      in
+      paren (pr_constructor kn ++ cl)
+    | _, GTydRec def ->
+      let args = List.combine def cl in
+      let pr_arg ((id, _, _), arg) =
+        let kn = change_kn_label tpe id in
+        pr_projection kn ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr E1 arg
+      in
+      let args = prlist_with_sep (fun () -> str ";" ++ spc ()) pr_arg args in
+      str "{" ++ spc () ++ args ++ spc () ++ str "}"
+    | _, GTydDef _ -> assert false
+    end
+  | GTacCse (e, info, cst_br, ncst_br) ->
+    let e = pr_glbexpr E5 e in
+    let br = match info with
+    | GCaseAlg kn ->
+      let def = match Tac2env.interp_type kn with
+      | _, GTydAlg def -> def
+      | _, GTydDef _ | _, GTydRec _ -> assert false
+      in
+      let br = order_branches cst_br ncst_br def in
+      let pr_branch (cstr, vars, p) =
+        let cstr = change_kn_label kn cstr in
+        let cstr = pr_constructor cstr in
+        let vars = match vars with
+        | [] -> mt ()
+        | _ -> spc () ++ pr_sequence pr_name vars
+        in
+        hov 0 (str "|" ++ spc () ++ cstr ++ vars ++ spc () ++ str "=>" ++ spc () ++
+          hov 2 (pr_glbexpr E5 p)) ++ spc ()
+      in
+      prlist pr_branch br
+    | GCaseTuple n ->
+      let (vars, p) = ncst_br.(0) in
+      let p = pr_glbexpr E5 p in
+      let vars = prvect_with_sep (fun () -> str "," ++ spc ()) pr_name vars in
+      str "|" ++ spc () ++ paren vars ++ spc () ++ str "=>" ++ spc () ++ p
+    in
+    hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end")
+  | GTacPrj (kn, e, n) ->
+    let def = match Tac2env.interp_type kn with
+    | _, GTydRec def -> def
+    | _, GTydDef _ | _, GTydAlg _ -> assert false
+    in
+    let (proj, _, _) = List.nth def n in
+    let proj = change_kn_label kn proj in
+    let proj = pr_projection proj in
+    let e = pr_glbexpr E0 e in
+    e ++ str "." ++ paren proj
+  | GTacSet (kn, e, n, r) ->
+    let def = match Tac2env.interp_type kn with
+    | _, GTydRec def -> def
+    | _, GTydDef _ | _, GTydAlg _ -> assert false
+    in
+    let (proj, _, _) = List.nth def n in
+    let proj = change_kn_label kn proj in
+    let proj = pr_projection proj in
+    let e = pr_glbexpr E0 e in
+    let r = pr_glbexpr E1 r in
+    e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r
+  | GTacExt arg ->
+    let GenArg (Glbwit tag, arg) = arg in
+    let name = match tag with
+    | ExtraArg tag -> ArgT.repr tag
+    | _ -> assert false
+    in
+    str name ++ str ":" ++ paren (Genprint.glb_print tag arg)
+  | GTacPrm (prm, args) ->
+    let args = match args with
+    | [] -> mt ()
+    | _ -> spc () ++ pr_sequence (pr_glbexpr E0) args
+    in
+    str "@external" ++ spc () ++ qstring prm.mltac_plugin ++ spc () ++
+      qstring prm.mltac_tactic ++ args
+  in
+  hov 0 (pr_glbexpr lvl c)
+
+let pr_glbexpr c =
+  pr_glbexpr_gen E5 c
diff --git a/tac2print.mli b/tac2print.mli
new file mode 100644
index 0000000000..94555a4c95
--- /dev/null
+++ b/tac2print.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Tac2expr
+
+(** {5 Printing types} *)
+
+val pr_typref : type_constant -> 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 : glb_tacexpr -> std_ppcmds
+
+(** {5 Utilities} *)
+
+val int_name : unit -> (int -> string)
+(** Create a function that give names to integers. The names are generated on
+    the fly, in the order they are encountered. *)