place all pretty-printing files in new dir printing/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 5102 insertions, 0 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
new file mode 100644
index 000000000..2e3ce2103
--- /dev/null
+++ b/printing/ppconstr.ml
@@ -0,0 +1,645 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i*)
+open Errors
+open Util
+open Pp
+open Names
+open Nameops
+open Libnames
+open Ppextend
+open Constrexpr
+open Constrexpr_ops
+open Topconstr
+open Term
+open Decl_kinds
+open Misctypes
+open Locus
+open Genredexpr
+(*i*)
+
+let sep_v = fun _ -> str"," ++ spc()
+let pr_tight_coma () = str "," ++ cut ()
+
+let latom = 0
+let lprod = 200
+let llambda = 200
+let lif = 200
+let lletin = 200
+let lletpattern = 200
+let lfix = 200
+let larrow = 90
+let lcast = 100
+let larg = 9
+let lapp = 10
+let lposint = 0
+let lnegint = 35 (* must be consistent with Notation "- x" *)
+let ltop = (200,E)
+let lproj = 1
+let lsimple = (1,E)
+
+let prec_less child (parent,assoc) =
+  if parent < 0 && child = lprod then true
+  else
+    let parent = abs parent in
+    match assoc with
+      | E -> (<=) child parent
+      | L -> (<) child parent
+      | Prec n -> child<=n
+      | Any -> true
+
+let prec_of_prim_token = function
+  | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+  | String _ -> latom
+
+open Notation
+
+let print_hunks n pr pr_binders (terms,termlists,binders) unp =
+  let env = ref terms and envlist = ref termlists and bll = ref binders in
+  let pop r = let a = List.hd !r in r := List.tl !r; a in
+  let rec aux = function
+  | [] -> mt ()
+  | UnpMetaVar (_,prec) :: l ->
+      let c = pop env in pr (n,prec) c ++ aux l
+  | UnpListMetaVar (_,prec,sl) :: l ->
+      let cl = pop envlist in
+      let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+      let pp2 = aux l in
+      pp1 ++ pp2
+  | UnpBinderListMetaVar (_,isopen,sl) :: l ->
+      let cl = pop bll in pr_binders (fun () -> aux sl) isopen cl ++ aux l
+  | UnpTerminal s :: l -> str s ++ aux l
+  | UnpBox (b,sub) :: l ->
+      (* Keep order: side-effects *)
+      let pp1 = ppcmd_of_box b (aux sub) in
+      let pp2 = aux l in
+      pp1 ++ pp2
+  | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
+  aux unp
+
+let pr_notation pr pr_binders s env =
+  let unpl, level = find_notation_printing_rule s in
+  print_hunks level pr pr_binders env unpl, level
+
+let pr_delimiters key strm =
+  strm ++ str ("%"^key)
+
+let pr_generalization bk ak c =
+  let hd, tl =
+    match bk with
+    | Implicit -> "{", "}"
+    | Explicit -> "(", ")"
+  in (* TODO: syntax Abstraction Kind *)
+    str "`" ++ str hd ++ c ++ str tl
+
+let pr_com_at n =
+  if Flags.do_beautify() && n <> 0 then comment n
+  else mt()
+
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+
+let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+
+let pr_glob_sort = function
+  | GProp -> str "Prop"
+  | GSet -> str "Set"
+  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment (fun x->x)) u)
+
+let pr_id = pr_id
+let pr_name = pr_name
+let pr_qualid = pr_qualid
+let pr_patvar = pr_id
+
+let pr_expl_args pr (a,expl) =
+  match expl with
+  | None -> pr (lapp,L) a
+  | Some (_,ExplByPos (n,_id)) ->
+      anomaly("Explicitation by position not implemented")
+  | Some (_,ExplByName id) ->
+      str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
+
+let pr_opt_type pr = function
+  | CHole _ -> mt ()
+  | t -> cut () ++ str ":" ++ pr t
+
+let pr_opt_type_spc pr = function
+  | CHole _ -> mt ()
+  | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+
+let pr_lident (loc,id) =
+  if loc <> dummy_loc then
+    let (b,_) = unloc loc in
+    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+  else pr_id id
+
+let pr_lname = function
+    (loc,Name id) -> pr_lident (loc,id)
+  | lna -> pr_located pr_name lna
+
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (loc,s) -> pr_lident (loc,s)
+
+let pr_prim_token = function
+  | Numeral n -> Bigint.pr_bigint n
+  | String s -> qs s
+
+let pr_evar pr n l =
+  hov 0 (str (Evd.string_of_existential n) ++
+  (match l with
+   | Some l ->
+       spc () ++ pr_in_comment
+         (fun l ->
+	   str"[" ++ hov 0 (prlist_with_sep pr_comma (pr ltop) l) ++ str"]")
+         (List.rev l)
+   | None -> mt()))
+
+let las = lapp
+let lpator = 100
+let lpatrec = 0
+
+let rec pr_patt sep inh p =
+  let (strm,prec) = match p with
+  | CPatRecord (_, l) ->
+      let pp (c, p) =
+	pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p in
+      str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
+  | CPatAlias (_,p,id) ->
+      pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
+  | CPatCstr (_,c,[]) -> pr_reference c, latom
+  | CPatCstr (_,c,args) ->
+      pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+  | CPatCstrExpl (_,c,args) ->
+      str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+  | CPatAtom (_,None) -> str "_", latom
+  | CPatAtom (_,Some r) -> pr_reference r, latom
+  | CPatOr (_,pl) ->
+      hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
+  | CPatNotation (_,"( _ )",([p],[])) ->
+      pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+  | CPatNotation (_,s,(l,ll)) ->
+      pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[])
+  | CPatPrim (_,p) -> pr_prim_token p, latom
+  | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
+  in
+  let loc = cases_pattern_expr_loc p in
+  pr_with_comments loc
+    (sep() ++ if prec_less prec inh then strm else surround strm)
+
+let pr_patt = pr_patt mt
+
+let pr_eqn pr (loc,pl,rhs) =
+  let pl = List.map snd pl in
+  spc() ++ hov 4
+    (pr_with_comments loc
+      (str "| " ++
+      hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
+             ++ str " =>") ++
+      pr_sep_com spc (pr ltop) rhs))
+
+let begin_of_binder = function
+    LocalRawDef((loc,_),_) -> fst (unloc loc)
+  | LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc)
+  | _ -> assert false
+
+let begin_of_binders = function
+  | b::_ -> begin_of_binder b
+  | _ -> 0
+
+let surround_impl k p =
+  match k with
+  | Explicit -> str"(" ++ p ++ str")"
+  | Implicit -> str"{" ++ p ++ str"}"
+
+let surround_implicit k p =
+  match k with
+  | Explicit -> p
+  | Implicit -> (str"{" ++ p ++ str"}")
+
+let pr_binder many pr (nal,k,t) =
+  match k with
+    | Generalized (b, b', t') ->
+      assert (b=Implicit);
+      begin match nal with
+	|[loc,Anonymous] ->
+	  hov 1 (str"`" ++ (surround_impl b'
+			      ((if t' then str "!" else mt ()) ++ pr t)))
+	|[loc,Name id] ->
+	  hov 1 (str "`" ++ (surround_impl b'
+			       (pr_lident (loc,id) ++ str " : " ++
+				  (if t' then str "!" else mt()) ++ pr t)))
+	|_ -> anomaly "List of generalized binders have alwais one element."
+      end
+    | Default b ->
+      match t with
+	| CHole _ ->
+	  let s = prlist_with_sep spc pr_lname nal in
+	  hov 1 (surround_implicit b s)
+	| _ ->
+	  let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in
+	  hov 1 (if many then surround_impl b s else surround_implicit b s)
+
+let pr_binder_among_many pr_c = function
+  | LocalRawAssum (nal,k,t) ->
+      pr_binder true pr_c (nal,k,t)
+  | LocalRawDef (na,c) ->
+      let c,topt = match c with
+        | CCast(_,c, (CastConv t|CastVM t)) -> c, t
+        | _ -> c, CHole (dummy_loc, None) in
+      surround (pr_lname na ++ pr_opt_type pr_c topt ++
+         str":=" ++ cut() ++ pr_c c)
+
+let pr_undelimited_binders sep pr_c =
+  prlist_with_sep sep (pr_binder_among_many pr_c)
+
+let pr_delimited_binders kw sep pr_c bl =
+  let n = begin_of_binders bl in
+  match bl with
+  | [LocalRawAssum (nal,k,t)] ->
+      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
+  | LocalRawAssum _ :: _ as bdl ->
+      pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
+  | _ -> assert false
+
+let pr_binders_gen pr_c sep is_open =
+  if is_open then pr_delimited_binders mt sep pr_c
+  else pr_undelimited_binders sep pr_c
+
+let rec extract_prod_binders = function
+(*  | CLetIn (loc,na,b,c) as x ->
+      let bl,c = extract_prod_binders c in
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+  | CProdN (loc,[],c) ->
+      extract_prod_binders c
+  | CProdN (loc,(nal,bk,t)::bl,c) ->
+      let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
+      LocalRawAssum (nal,bk,t) :: bl, c
+  | c -> [], c
+
+let rec extract_lam_binders = function
+(*  | CLetIn (loc,na,b,c) as x ->
+      let bl,c = extract_lam_binders c in
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+  | CLambdaN (loc,[],c) ->
+      extract_lam_binders c
+  | CLambdaN (loc,(nal,bk,t)::bl,c) ->
+      let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
+      LocalRawAssum (nal,bk,t) :: bl, c
+  | c -> [], c
+
+let split_lambda = function
+  | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
+  | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+  | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let rename na na' t c =
+  match (na,na') with
+    | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
+    | (_,Name id), (_,Anonymous) -> (na,t,c)
+    | _ -> (na',t,c)
+
+let split_product na' = function
+  | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
+  | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,bk,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let rec split_fix n typ def =
+  if n = 0 then ([],typ,def)
+  else
+    let (na,_,def) = split_lambda def in
+    let (na,t,typ) = split_product na typ in
+    let (bl,typ,def) = split_fix (n-1) typ def in
+    (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
+
+let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
+  let pr_body =
+    if dangling_with_for then pr_dangling else pr in
+  pr_id id ++ str" " ++
+  hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
+  pr_opt_type_spc pr t ++ str " :=" ++
+  pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
+
+let pr_guard_annot pr_aux bl (n,ro) =
+  match n with
+    | None -> mt ()
+    | Some (loc, id) ->
+      match (ro : Constrexpr.recursion_order_expr) with
+	| CStructRec ->
+	  let names_of_binder = function
+	    | LocalRawAssum (nal,_,_) -> nal
+	    | LocalRawDef (_,_) -> []
+	  in let ids = List.flatten (List.map names_of_binder bl) in
+	     if List.length ids > 1 then
+	       spc() ++ str "{struct " ++ pr_id id ++ str"}"
+	     else mt()
+	| CWfRec c ->
+	  spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
+	| CMeasureRec (m,r) ->
+	  spc() ++ str "{measure " ++ pr_aux m ++ spc() ++ pr_id id++
+	    (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
+
+let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+  let annot = pr_guard_annot (pr lsimple) bl ro in
+    pr_recursive_decl pr prd dangling_with_for id bl annot t c
+
+let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
+  pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
+
+let pr_recursive pr_decl id = function
+  | [] -> anomaly "(co)fixpoint with no definition"
+  | [d1] -> pr_decl false d1
+  | dl ->
+      prlist_with_sep (fun () -> fnl() ++ str "with ")
+        (pr_decl true) dl ++
+      fnl() ++ str "for " ++ pr_id id
+
+let pr_asin pr (na,indnalopt) =
+  (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
+    | Some na -> spc () ++ str "as " ++  pr_lname na
+    | None -> mt ()) ++
+  (match indnalopt with
+    | None -> mt ()
+    | Some t -> spc () ++ str "in " ++ pr_patt lsimple t)
+
+let pr_case_item pr (tm,asin) =
+  hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+
+let pr_case_type pr po =
+  match po with
+    | None | Some (CHole _) -> mt()
+    | Some p ->
+        spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
+
+let pr_simple_return_type pr na po =
+  (match na with
+    | Some (_,Name id) ->
+        spc () ++ str "as " ++  pr_id id
+    | _ -> mt ()) ++
+  pr_case_type pr po
+
+let pr_proj pr pr_app a f l =
+  hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+
+let pr_appexpl pr f l =
+      hov 2 (
+	str "@" ++ pr_reference f ++
+	prlist (pr_sep_com spc (pr (lapp,L))) l)
+
+let pr_app pr a l =
+  hov 2 (
+    pr (lapp,L) a  ++
+    prlist (fun a -> spc () ++ pr_expl_args pr a) l)
+
+let pr_forall () = str"forall" ++ spc ()
+
+let pr_fun () = str"fun" ++ spc ()
+
+let pr_fun_sep = str " =>"
+
+
+let pr_dangling_with_for sep pr inherited a =
+  match a with
+  | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a
+  | _ -> pr sep inherited a
+
+let pr pr sep inherited a =
+  let (strm,prec) = match a with
+  | CRef r -> pr_reference r, latom
+  | CFix (_,id,fix) ->
+      hov 0 (str"fix " ++
+             pr_recursive
+               (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
+      lfix
+  | CCoFix (_,id,cofix) ->
+      hov 0 (str "cofix " ++
+             pr_recursive
+              (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
+      lfix
+  | CProdN _ ->
+      let (bl,a) = extract_prod_binders a in
+      hov 0 (
+	hov 2 (pr_delimited_binders pr_forall spc
+                 (pr mt ltop) bl) ++
+        str "," ++ pr spc ltop a),
+      lprod
+  | CLambdaN _ ->
+      let (bl,a) = extract_lam_binders a in
+      hov 0 (
+        hov 2 (pr_delimited_binders pr_fun spc
+                (pr mt ltop) bl) ++
+	       pr_fun_sep ++ pr spc ltop a),
+      llambda
+  | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+      when x=x' ->
+      hv 0 (
+        hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++
+        pr spc ltop b),
+      lletin
+  | CLetIn (_,x,a,b) ->
+      hv 0 (
+        hov 2 (str "let " ++ pr_lname x ++ str " :=" ++
+               pr spc ltop a ++ str " in") ++
+        pr spc ltop b),
+      lletin
+  | CAppExpl (_,(Some i,f),l) ->
+      let l1,l2 = list_chop i l in
+      let c,l1 = list_sep_last l1 in
+      let p = pr_proj (pr mt) pr_appexpl c f l1 in
+      if l2<>[] then
+	p ++ prlist (pr spc (lapp,L)) l2, lapp
+      else
+	p, lproj
+  | CAppExpl (_,(None,Ident (_,var)),[t])
+  | CApp (_,(_,CRef(Ident(_,var))),[t,None])
+        when var = Notation_ops.ldots_var ->
+      hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
+  | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
+  | CApp (_,(Some i,f),l) ->
+      let l1,l2 = list_chop i l in
+      let c,l1 = list_sep_last l1 in
+      assert (snd c = None);
+      let p = pr_proj (pr mt) pr_app (fst c) f l1 in
+      if l2<>[] then
+	p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
+      else
+	p, lproj
+  | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
+  | CRecord (_,w,l) ->
+      let beg =
+	match w with
+	| None -> spc ()
+	| Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
+      in
+	hv 0 (str"{|" ++ beg ++
+	      prlist_with_sep pr_semicolon
+		(fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
+	      ++ str" |}"), latom
+
+  | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+      hv 0 (
+	str "let '" ++
+	  hov 0 (pr_patt ltop p ++
+		 pr_asin (pr_dangling_with_for mt pr) asin ++
+		 str " :=" ++ pr spc ltop c ++
+		 pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
+		 str " in" ++ pr spc ltop b)),
+	lletpattern
+  | CCases(_,_,rtntypopt,c,eqns) ->
+      v 0
+        (hv 0 (str "match" ++ brk (1,2) ++
+		  hov 0 (
+		    prlist_with_sep sep_v
+		      (pr_case_item (pr_dangling_with_for mt pr)) c
+		    ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++
+		  spc () ++ str "with") ++
+		  prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
+      latom
+  | CLetTuple (_,nal,(na,po),c,b) ->
+      hv 0 (
+        str "let " ++
+	hov 0 (str "(" ++
+               prlist_with_sep sep_v pr_lname nal ++
+               str ")" ++
+	       pr_simple_return_type (pr mt) na po ++ str " :=" ++
+               pr spc ltop c ++ str " in") ++
+        pr spc ltop b),
+      lletin
+  | CIf (_,c,(na,po),b1,b2) ->
+      (* On force les parenthèses autour d'un "if" sous-terme (même si le
+	 parsing est lui plus tolérant) *)
+      hv 0 (
+	hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++
+	spc () ++
+	hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+	hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
+      lif
+
+  | CHole _ -> str "_", latom
+  | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
+  | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
+  | CSort (_,s) -> pr_glob_sort s, latom
+  | CCast (_,a,b) ->
+      hv 0 (pr mt (lcast,L) a ++ cut () ++
+	    match b with
+	      | CastConv b -> str ":" ++ pr mt (-lcast,E) b
+	      | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
+	      | CastCoerce -> str ":>"), lcast
+  | CNotation (_,"( _ )",([t],[],[])) ->
+      pr (fun()->str"(") (max_int,L) t ++ str")", latom
+  | CNotation (_,s,env) ->
+      pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
+  | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
+  | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
+  in
+  let loc = constr_loc a in
+  pr_with_comments loc
+    (sep() ++ if prec_less prec inherited then strm else surround strm)
+
+type term_pr = {
+  pr_constr_expr   : constr_expr -> std_ppcmds;
+  pr_lconstr_expr  : constr_expr -> std_ppcmds;
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+}
+
+type precedence =  Ppextend.precedence * Ppextend.parenRelation
+let modular_constr_pr = pr
+let rec fix rf x =rf (fix rf) x
+let pr = fix modular_constr_pr mt
+
+let default_term_pr = {
+  pr_constr_expr   = pr lsimple;
+  pr_lconstr_expr  = pr ltop;
+  pr_constr_pattern_expr  = pr lsimple;
+  pr_lconstr_pattern_expr = pr ltop
+}
+
+let term_pr = ref default_term_pr
+
+let set_term_pr = (:=) term_pr
+
+let pr_constr_expr c   = !term_pr.pr_constr_expr   c
+let pr_lconstr_expr c  = !term_pr.pr_lconstr_expr  c
+let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
+let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
+
+let pr_cases_pattern_expr = pr_patt ltop
+
+let pr_binders = pr_undelimited_binders spc (pr ltop)
+
+let pr_with_occurrences pr (occs,c) =
+  match occs with
+    | AllOccurrences -> pr c
+    | NoOccurrences -> failwith "pr_with_occurrences: no occurrences"
+    | OnlyOccurrences nl ->
+      hov 1 (pr c ++ spc() ++ str"at " ++
+        hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+    | AllOccurrencesBut nl ->
+      hov 1 (pr c ++ spc() ++ str"at - " ++
+        hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+let pr_red_flag pr r =
+  (if r.rBeta then pr_arg str "beta" else mt ()) ++
+  (if r.rIota then pr_arg str "iota" else mt ()) ++
+  (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+  (if r.rConst = [] then
+     if r.rDelta then pr_arg str "delta"
+     else mt ()
+   else
+     pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+     hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+open Genarg
+
+let pr_metaid id = str"?" ++ pr_id id
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
+  | Red false -> str "red"
+  | Hnf -> str "hnf"
+  | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o
+  | Cbv f ->
+      if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
+	str "compute"
+      else
+	hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
+  | Lazy f ->
+      hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
+  | Unfold l ->
+      hov 1 (str "unfold" ++ spc() ++
+             prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
+  | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
+  | Pattern l ->
+      hov 1 (str "pattern" ++
+        pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)
+
+  | Red true -> error "Shouldn't be accessible from user."
+  | ExtraRedExpr s -> str s
+  | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
+
+let rec pr_may_eval test prc prlc pr2 pr3 = function
+  | ConstrEval (r,c) ->
+      hov 0
+        (str "eval" ++ brk (1,1) ++
+         pr_red_expr (prc,prlc,pr2,pr3) r ++
+	 str " in" ++ spc() ++ prc c)
+  | ConstrContext ((_,id),c) ->
+      hov 0
+	(str "context " ++ pr_id id ++ spc () ++
+	 str "[" ++ prlc c ++ str "]")
+  | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c)
+  | ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")")
+  | ConstrTerm c -> prc c
+
+let pr_may_eval a = pr_may_eval (fun _ -> false) a
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
new file mode 100644
index 000000000..6453c26f4
--- /dev/null
+++ b/printing/ppconstr.mli
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Environ
+open Term
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
+open Locus
+open Genredexpr
+
+val extract_lam_binders :
+  constr_expr -> local_binder list * constr_expr
+val extract_prod_binders :
+  constr_expr -> local_binder list * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr ->
+  local_binder list *  constr_expr * constr_expr
+
+val prec_less : int -> int * Ppextend.parenRelation -> bool
+
+val pr_tight_coma : unit -> std_ppcmds
+
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_metaid : identifier -> std_ppcmds
+
+val pr_lident : identifier located -> std_ppcmds
+val pr_lname : name located -> std_ppcmds
+
+val pr_with_comments : loc -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+val pr_sep_com :
+  (unit -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  constr_expr -> std_ppcmds
+
+val pr_id : identifier -> std_ppcmds
+val pr_name : name -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
+
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+  ('a,'b,'c) red_expr_gen -> std_ppcmds
+val pr_may_eval :
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
+
+val pr_glob_sort : glob_sort -> std_ppcmds
+val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+  local_binder list ->
+  ('a * Names.identifier) option * recursion_order_expr ->
+  std_ppcmds
+
+val pr_binders : local_binder list -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_constr_expr : constr_expr -> std_ppcmds
+val pr_lconstr_expr : constr_expr -> std_ppcmds
+val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+type term_pr = {
+  pr_constr_expr   : constr_expr -> std_ppcmds;
+  pr_lconstr_expr  : constr_expr -> std_ppcmds;
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+}
+
+val set_term_pr : term_pr -> unit
+val default_term_pr : term_pr
+
+(** The modular constr printer.
+    [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+    [pr] on its subterms.
+    [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop]
+    for "lconstr" printers (spiwack: we might need more specification here).
+    We can make a new modular constr printer by overriding certain branches,
+    for instance if we want to build a printer which prints "Prop" as "Omega"
+    instead we can proceed as follows:
+    let my_modular_constr_pr pr s p = function
+      | CSort (_,GProp Null) -> str "Omega"
+      | t -> modular_constr_pr pr s p t
+    Which has the same type. We can turn a modular printer into a printer by
+    taking its fixpoint. *)
+
+type precedence
+val lsimple : precedence
+val ltop : precedence
+val modular_constr_pr :
+               ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
+                (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
diff --git a/printing/ppextra.ml b/printing/ppextra.ml
new file mode 100644
index 000000000..a85cafd40
--- /dev/null
+++ b/printing/ppextra.ml
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Ppextend
+open Pptactic
+open Extrawit
+
+let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
+
+let _ = for i=0 to 5 do
+  declare_extra_genarg_pprule
+  (rawwit_tactic i, pr_tac_polymorphic i)
+  (globwit_tactic i, pr_tac_polymorphic i)
+  (wit_tactic i, pr_tac_polymorphic i)
+done
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
new file mode 100644
index 000000000..14cfe2ffc
--- /dev/null
+++ b/printing/pptactic.ml
@@ -0,0 +1,1048 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Namegen
+open Errors
+open Util
+open Constrexpr
+open Tacexpr
+open Genarg
+open Libnames
+open Ppextend
+open Misctypes
+open Miscops
+open Locus
+open Decl_kinds
+open Genredexpr
+open Ppconstr
+open Printer
+
+let pr_global x = Nametab.pr_global_env Idset.empty x
+
+type grammar_terminals = string option list
+
+  (* Extensions *)
+let prtac_tab = Hashtbl.create 17
+
+let declare_extra_tactic_pprule (s,tags,prods) =
+  Hashtbl.add prtac_tab (s,tags) prods
+
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
+
+type 'a raw_extra_genarg_printer =
+    (constr_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) ->
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+type 'a glob_extra_genarg_printer =
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+type 'a extra_genarg_printer =
+    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+let genarg_pprule = ref Stringmap.empty
+
+let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
+  let s = match unquote wit with
+    | ExtraArgType s -> s
+    | _ -> error
+	"Can declare a pretty-printing rule only for extra argument types."
+  in
+  let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
+  let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
+  let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
+  genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
+
+let pr_arg pr x = spc () ++ pr x
+
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (_,s) -> pr_id s
+
+let pr_or_metaid pr = function
+  | AI x -> pr x
+  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"
+
+let pr_and_short_name pr (c,_) = pr c
+
+let pr_or_by_notation f = function
+  | AN v -> f v
+  | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+let pr_located pr (loc,x) = pr x
+
+let pr_evaluable_reference = function
+  | EvalVarRef id -> pr_id id
+  | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+
+let pr_quantified_hypothesis = function
+  | AnonHyp n -> int n
+  | NamedHyp id -> pr_id id
+
+let pr_binding prc = function
+  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+  | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+  | ImplicitBindings l ->
+      brk (1,1) ++ str "with" ++ brk (1,1) ++
+      prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+      brk (1,1) ++ str "with" ++ brk (1,1) ++
+        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+  | ImplicitBindings l ->
+      brk (1,1) ++
+      prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+      brk (1,1) ++
+        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+  prc c ++ hv 0 (pr_bindings prc prlc bl)
+
+let pr_with_constr prc = function
+  | None -> mt ()
+  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
+let rec pr_message_token prid = function
+  | MsgString s -> qs s
+  | MsgInt n -> int n
+  | MsgIdent id -> prid id
+
+let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
+
+let with_evars ev s = if ev then "e" ^ s else s
+
+let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
+
+let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
+  match Genarg.genarg_tag x with
+  | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen rawwit_int x)
+  | IntOrVarArgType -> pr_or_var int (out_gen rawwit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
+  | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
+  | RefArgType -> prref (out_gen rawwit_ref x)
+  | SortArgType -> pr_glob_sort (out_gen rawwit_sort x)
+  | ConstrArgType -> prc (out_gen rawwit_constr x)
+  | ConstrMayEvalArgType ->
+      pr_may_eval prc prlc (pr_or_by_notation prref) prpat
+        (out_gen rawwit_constr_may_eval x)
+  | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
+  | RedExprArgType ->
+      pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
+        (out_gen rawwit_red_expr x)
+  | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x))
+  | ConstrWithBindingsArgType ->
+      pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x)
+  | BindingsArgType ->
+      pr_bindings_no_with prc prlc (out_gen rawwit_bindings x)
+  | List0ArgType _ ->
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
+	(fold_list0 (fun a l -> a::l) x []))
+  | List1ArgType _ ->
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
+	(fold_list1 (fun a l -> a::l) x []))
+  | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prpat prref) (mt()) x)
+  | PairArgType _ ->
+      hov 0
+        (fold_pair
+	  (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
+            [a;b])
+	  x)
+  | ExtraArgType s ->
+      try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+
+
+let rec pr_glob_generic prc prlc prtac prpat x =
+  match Genarg.genarg_tag x with
+  | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen globwit_int x)
+  | IntOrVarArgType -> pr_or_var int (out_gen globwit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen globwit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
+  | VarArgType -> pr_located pr_id (out_gen globwit_var x)
+  | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
+  | SortArgType -> pr_glob_sort (out_gen globwit_sort x)
+  | ConstrArgType -> prc (out_gen globwit_constr x)
+  | ConstrMayEvalArgType ->
+      pr_may_eval prc prlc
+        (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
+        (out_gen globwit_constr_may_eval x)
+  | QuantHypArgType ->
+      pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
+  | RedExprArgType ->
+      pr_red_expr
+        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
+        (out_gen globwit_red_expr x)
+  | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x))
+  | ConstrWithBindingsArgType ->
+      pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x)
+  | BindingsArgType ->
+      pr_bindings_no_with prc prlc (out_gen globwit_bindings x)
+  | List0ArgType _ ->
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac prpat)
+	(fold_list0 (fun a l -> a::l) x []))
+  | List1ArgType _ ->
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac prpat)
+	(fold_list1 (fun a l -> a::l) x []))
+  | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac prpat) (mt()) x)
+  | PairArgType _ ->
+      hov 0
+        (fold_pair
+	  (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac prpat) [a;b])
+	  x)
+  | ExtraArgType s ->
+      try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+
+open Closure
+
+let rec pr_generic prc prlc prtac prpat x =
+  match Genarg.genarg_tag x with
+  | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
+  | IntArgType -> int (out_gen wit_int x)
+  | IntOrVarArgType -> pr_or_var int (out_gen wit_int_or_var x)
+  | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
+  | PreIdentArgType -> str (out_gen wit_pre_ident x)
+  | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
+  | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x)
+  | VarArgType -> pr_id (out_gen wit_var x)
+  | RefArgType -> pr_global (out_gen wit_ref x)
+  | SortArgType -> pr_sort (out_gen wit_sort x)
+  | ConstrArgType -> prc (out_gen wit_constr x)
+  | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x)
+  | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x)
+  | RedExprArgType ->
+      pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
+        (out_gen wit_red_expr x)
+  | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
+  | ConstrWithBindingsArgType ->
+      let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in
+      pr_with_bindings prc prlc (c,b)
+  | BindingsArgType ->
+      pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it
+  | List0ArgType _ ->
+      hov 0 (pr_sequence (pr_generic prc prlc prtac prpat)
+	(fold_list0 (fun a l -> a::l) x []))
+  | List1ArgType _ ->
+      hov 0 (pr_sequence (pr_generic prc prlc prtac prpat)
+	(fold_list1 (fun a l -> a::l) x []))
+  | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac prpat) (mt()) x)
+  | PairArgType _ ->
+      hov 0
+        (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac prpat)
+          [a;b])
+	  x)
+  | ExtraArgType s ->
+      try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+
+let rec tacarg_using_rule_token pr_gen = function
+  | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
+  | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al)
+  | [], [] -> []
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_tacarg_using_rule pr_gen l=
+  pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l)
+
+let pr_extend_gen pr_gen lev s l =
+  try
+    let tags = List.map genarg_tag l in
+    let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+    let p = pr_tacarg_using_rule pr_gen (pl,l) in
+    if lev' > lev then surround p else p
+  with Not_found ->
+    str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+
+let pr_raw_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+let pr_glob_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_glob_generic prc prlc prtac prpat)
+let pr_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_generic prc prlc prtac prpat)
+
+(**********************************************************************)
+(* The tactic printer                                                 *)
+
+let strip_prod_binders_expr n ty =
+  let rec strip_ty acc n ty =
+    match ty with
+        Constrexpr.CProdN(_,bll,a) ->
+          let nb =
+            List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
+	  let bll = List.map (fun (x, _, y) -> x, y) bll in
+            if nb >= n then (List.rev (bll@acc)), a
+            else strip_ty (bll@acc) (n-nb) a
+      | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let pr_ltac_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+
+let pr_ltac_constant sp =
+  pr_qualid (Nametab.shortest_qualid_of_tactic sp)
+
+let pr_evaluable_reference_env env = function
+  | EvalVarRef id -> pr_id id
+  | EvalConstRef sp ->
+      Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
+
+let pr_esubst prc l =
+  let pr_qhyp = function
+      (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+    | (_,NamedHyp id,c) ->
+        str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
+  in
+  prlist_with_sep spc pr_qhyp l
+
+let pr_bindings_gen for_ex prlc prc = function
+  | ImplicitBindings l ->
+      spc () ++
+      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+            prlist_with_sep spc prc l)
+  | ExplicitBindings l ->
+      spc () ++
+      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+            pr_esubst prlc l)
+  | NoBindings -> mt ()
+
+let pr_bindings prlc prc = pr_bindings_gen false prlc prc
+
+let pr_with_bindings prlc prc (c,bl) =
+  hov 1 (prc c ++ pr_bindings prlc prc bl)
+
+let pr_with_induction_names = function
+  | None, None -> mt ()
+  | eqpat, ipat ->
+      spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++
+                       pr_opt pr_intro_pattern ipat)
+
+let pr_as_intro_pattern ipat =
+  spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+let pr_with_inversion_names = function
+  | None -> mt ()
+  | Some ipat -> pr_as_intro_pattern ipat
+
+let pr_as_ipat = function
+  | None -> mt ()
+  | Some ipat -> pr_as_intro_pattern ipat
+
+let pr_as_name = function
+  | Anonymous -> mt ()
+  | Name id -> str " as " ++ pr_lident (dummy_loc,id)
+
+let pr_pose_as_style prc na c =
+  spc() ++ prc c ++ pr_as_name na
+
+let pr_pose prlc prc na c = match na with
+  | Anonymous -> spc() ++ prc c
+  | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+let pr_assertion _prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | IntroIdentifier id ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_as_ipat ipat
+
+let pr_assumption prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | IntroIdentifier id ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_as_ipat ipat
+
+let pr_by_tactic prt = function
+  | TacId [] -> mt ()
+  | tac -> spc() ++ str "by " ++ prt tac
+
+let pr_hyp_location pr_id = function
+  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+  | occs, InHypTypeOnly ->
+      spc () ++
+      pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
+  | occs, InHypValueOnly ->
+      spc () ++
+      pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
+
+let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+
+let pr_simple_hyp_clause pr_id = function
+  | [] -> mt ()
+  | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+let pr_in_hyp_as pr_id = function
+  | None -> mt ()
+  | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat
+
+let pr_clauses default_is_concl pr_id = function
+  | { onhyps=Some []; concl_occs=AllOccurrences }
+      when default_is_concl = Some true -> mt ()
+  | { onhyps=None; concl_occs=AllOccurrences }
+      when default_is_concl = Some false -> mt ()
+  | { onhyps=None; concl_occs=occs } ->
+      if occs = NoOccurrences then pr_in (str " * |-")
+      else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
+  | { onhyps=Some l; concl_occs=occs } ->
+      pr_in
+        (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++
+	 (if occs = NoOccurrences then mt ()
+	  else pr_with_occurrences (fun () -> str" |- *") (occs,())))
+
+let pr_orient b = if b then mt () else str " <-"
+
+let pr_multi = function
+  | Precisely 1 -> mt ()
+  | Precisely n -> int n ++ str "!"
+  | UpTo n -> int n ++ str "?"
+  | RepeatStar -> str "?"
+  | RepeatPlus -> str "!"
+
+let pr_induction_arg prlc prc = function
+  | ElimOnConstr c -> pr_with_bindings prlc prc c
+  | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+  | ElimOnAnonHyp n -> int n
+
+let pr_induction_kind = function
+  | SimpleInversion -> str "simple inversion"
+  | FullInversion -> str "inversion"
+  | FullInversionClear -> str "inversion_clear"
+
+let pr_lazy lz = if lz then str "lazy" else mt ()
+
+let pr_match_pattern pr_pat = function
+  | Term a -> pr_pat a
+  | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]"
+  | Subterm (b,Some id,a) ->
+      (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+
+let pr_match_hyps pr_pat = function
+  | Hyp (nal,mp) ->
+      pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Def (nal,mv,mp) ->
+      pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+      ++ str ":" ++ pr_match_pattern pr_pat mp
+
+let pr_match_rule m pr pr_pat = function
+  | Pat ([],mp,t) when m ->
+      pr_match_pattern pr_pat mp ++
+      spc () ++ str "=>" ++ brk (1,4) ++ pr t
+(*
+  | Pat (rl,mp,t) ->
+      hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
+        (if rl <> [] then spc () else mt ()) ++
+         hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+	 str "=>" ++ brk (1,4) ++ pr t))
+*)
+  | Pat (rl,mp,t) ->
+      hov 0 (
+	hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
+        (if rl <> [] then spc () else mt ()) ++
+        hov 0 (
+	  str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+	  str "=>" ++ brk (1,4) ++ pr t))
+  | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+
+let pr_funvar = function
+  | None -> spc () ++ str "_"
+  | Some id -> spc () ++ pr_id id
+
+let pr_let_clause k pr (id,(bl,t)) =
+  hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
+         str " :=" ++ brk (1,1) ++ pr (TacArg (dummy_loc,t)))
+
+let pr_let_clauses recflag pr = function
+  | hd::tl ->
+      hv 0
+        (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
+  | [] -> anomaly "LetIn must declare at least one binding"
+
+let pr_seq_body pr tl =
+  hv 0 (str "[ " ++
+        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+        str " ]")
+
+let pr_opt_tactic pr = function
+  | TacId [] -> mt ()
+  | t -> pr t
+
+let pr_then_gen pr tf tm tl =
+  hv 0 (str "[ " ++
+        prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+	pr_opt_tactic pr tm ++ str ".." ++
+	prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl ++
+        str " ]")
+
+let pr_hintbases = function
+  | None -> spc () ++ str "with *"
+  | Some [] -> mt ()
+  | Some l ->
+      spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l)
+
+let pr_auto_using prc = function
+  | [] -> mt ()
+  | l -> spc () ++
+      hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+
+let string_of_debug = function
+  | Off -> ""
+  | Debug -> "debug "
+  | Info -> "info_"
+
+let pr_then () = str ";"
+
+let ltop = (5,E)
+let lseq = 4
+let ltactical = 3
+let lorelse = 2
+let llet = 5
+let lfun = 5
+let lcomplete = 1
+let labstract = 3
+let lmatch = 1
+let latom = 0
+let lcall = 1
+let leval = 1
+let ltatom = 1
+let linfo = 5
+
+let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+
+open Closure
+
+(** A printer for tactics that polymorphically works on the three
+    "raw", "glob" and "typed" levels; in practice, the environment is
+    used only at the glob and typed level: it is used to feed the
+    constr printers *)
+
+let make_pr_tac
+  (pr_tac_level,pr_constr,pr_lconstr,pr_pat,
+   pr_cst,pr_ind,pr_ref,pr_ident,
+   pr_extend,strip_prod_binders) env =
+
+(* The environment is not used by the tactic printer: it is passed to the
+   constr and cst printers; hence we can make some abbreviations *)
+let pr_constr = pr_constr env in
+let pr_lconstr = pr_lconstr env in
+let pr_lpat = pr_pat true in
+let pr_pat = pr_pat false in
+let pr_cst = pr_cst env in
+let pr_ind = pr_ind env in
+let pr_tac_level = pr_tac_level env in
+
+(* Other short cuts *)
+let pr_bindings = pr_bindings pr_lconstr pr_constr in
+let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
+let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
+let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
+let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
+
+let pr_constrarg c = spc () ++ pr_constr c in
+let pr_lconstrarg c = spc () ++ pr_lconstr c in
+let pr_intarg n = spc () ++ int n in
+
+(* Some printing combinators *)
+let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
+
+let extract_binders = function
+  | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+  | body -> ([],body) in
+
+let pr_binder_fix (nal,t) =
+(*  match t with
+  | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+  | _ ->*)
+    let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr_lconstr t in
+    spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+let pr_fix_tac (id,n,c) =
+  let rec set_nth_name avoid n = function
+      (nal,ty)::bll ->
+        if n <= List.length nal then
+          match list_chop (n-1) nal with
+              _, (_,Name id) :: _ -> id, (nal,ty)::bll
+            | bef, (loc,Anonymous) :: aft ->
+                let id = next_ident_away (id_of_string"y") avoid in
+                id, ((bef@(loc,Name id)::aft, ty)::bll)
+            | _ -> assert false
+        else
+          let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+          (id,(nal,ty)::bll')
+    | [] -> assert false in
+  let (bll,ty) = strip_prod_binders n c in
+  let names =
+    List.fold_left
+      (fun ln (nal,_) -> List.fold_left
+          (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+          ln nal)
+      [] bll in
+  let idarg,bll = set_nth_name names n bll in
+  let annot =
+    if List.length names = 1 then mt()
+    else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
+  hov 1 (str"(" ++ pr_id id ++
+        prlist pr_binder_fix bll ++ annot ++ str" :" ++
+        pr_lconstrarg ty ++ str")") in
+(*  spc() ++
+  hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+    c)
+*)
+let pr_cofix_tac (id,c) =
+  hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+  (* Printing tactics as arguments *)
+let rec pr_atom0 = function
+  | TacIntroPattern [] -> str "intros"
+  | TacIntroMove (None,MoveLast) -> str "intro"
+  | TacAssumption -> str "assumption"
+  | TacAnyConstructor (false,None) -> str "constructor"
+  | TacAnyConstructor (true,None) -> str "econstructor"
+  | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
+  | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
+  | TacReflexivity -> str "reflexivity"
+  | TacClear (true,[]) -> str "clear"
+  | t -> str "(" ++ pr_atom1 t ++ str ")"
+
+  (* Main tactic printer *)
+and pr_atom1 = function
+  | TacExtend (loc,s,l) ->
+      pr_with_comments loc (pr_extend 1 s l)
+  | TacAlias (loc,s,l,_) ->
+      pr_with_comments loc (pr_extend 1 s (List.map snd l))
+
+  (* Basic tactics *)
+  | TacIntroPattern [] as t -> pr_atom0 t
+  | TacIntroPattern (_::_ as p) ->
+      hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
+  | TacIntrosUntil h ->
+      hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
+  | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
+  | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
+  | TacIntroMove (ido,hto) ->
+      hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
+  | TacAssumption as t -> pr_atom0 t
+  | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
+  | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
+  | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
+  | TacApply (a,ev,cb,inhyp) ->
+      hov 1 ((if a then mt() else str "simple ") ++
+             str (with_evars ev "apply") ++ spc () ++
+             prlist_with_sep pr_comma pr_with_bindings cb ++
+             pr_in_hyp_as pr_ident inhyp)
+  | TacElim (ev,cb,cbo) ->
+      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
+        pr_opt pr_eliminator cbo)
+  | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
+  | TacCase (ev,cb) ->
+      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
+  | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
+  | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+  | TacMutualFix (hidden,id,n,l) ->
+      if hidden then str "idtac" (* should caught before! *) else
+      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
+             str"with " ++ prlist_with_sep spc pr_fix_tac l)
+  | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
+  | TacMutualCofix (hidden,id,l) ->
+      if hidden then str "idtac" (* should be caught before! *) else
+      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
+             str"with " ++ prlist_with_sep spc pr_cofix_tac l)
+  | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
+  | TacAssert (Some tac,ipat,c) ->
+      hov 1 (str "assert" ++
+             pr_assumption pr_lconstr pr_constr ipat c ++
+             pr_by_tactic (pr_tac_level ltop) tac)
+  | TacAssert (None,ipat,c) ->
+      hov 1 (str "pose proof" ++
+             pr_assertion pr_lconstr pr_constr ipat c)
+  | TacGeneralize l ->
+      hov 1 (str "generalize" ++ spc () ++
+             prlist_with_sep pr_comma (fun (cl,na) ->
+	       pr_with_occurrences pr_constr cl ++ pr_as_name na)
+	     l)
+  | TacGeneralizeDep c ->
+      hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
+             pr_constrarg c)
+  | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere ->
+      hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
+  | TacLetTac (na,c,cl,b) ->
+      hov 1 ((if b then str "set" else str "remember") ++
+             (if b then pr_pose pr_lconstr else pr_pose_as_style)
+	        pr_constr na c ++
+             pr_clauses (Some b) pr_ident cl)
+(*  | TacInstantiate (n,c,ConclLocation ()) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg c ++ str ")" ))
+  | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg c ++ str ")" )
+	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+*)
+  (* Derived basic tactics *)
+  | TacSimpleInductionDestruct (isrec,h) ->
+      hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
+             ++ pr_arg pr_quantified_hypothesis h)
+  | TacInductionDestruct (isrec,ev,(l,cl)) ->
+      hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
+             spc () ++
+             prlist_with_sep pr_comma (fun (h,e,ids) ->
+	       prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
+	       pr_with_induction_names ids ++
+               pr_opt pr_eliminator e) l ++
+               pr_opt_no_spc (pr_clauses None pr_ident) cl)
+  | TacDoubleInduction (h1,h2) ->
+      hov 1
+        (str "double induction" ++
+         pr_arg pr_quantified_hypothesis h1 ++
+	 pr_arg pr_quantified_hypothesis h2)
+  | TacDecomposeAnd c ->
+      hov 1 (str "decompose record" ++ pr_constrarg c)
+  | TacDecomposeOr c ->
+      hov 1 (str "decompose sum" ++ pr_constrarg c)
+  | TacDecompose (l,c) ->
+      hov 1 (str "decompose" ++ spc () ++
+        hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
+	  ++ str "]" ++ pr_constrarg c))
+  | TacSpecialize (n,c) ->
+      hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
+             pr_with_bindings c)
+  | TacLApply c ->
+      hov 1 (str "lapply" ++ pr_constrarg c)
+
+  (* Automation tactics *)
+  | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+  | TacTrivial (d,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "trivial") ++
+             pr_auto_using pr_constr lems ++ pr_hintbases db)
+  | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
+  | TacAuto (d,n,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "auto") ++
+	     pr_opt (pr_or_var int) n ++
+             pr_auto_using pr_constr lems ++ pr_hintbases db)
+
+  (* Context management *)
+  | TacClear (true,[]) as t -> pr_atom0 t
+  | TacClear (keep,l) ->
+      hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
+             prlist_with_sep spc pr_ident l)
+  | TacClearBody l ->
+      hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
+  | TacMove (b,id1,id2) ->
+      (* Rem: only b = true is available for users *)
+      assert b;
+      hov 1
+        (str "move" ++ brk (1,1) ++ pr_ident id1 ++
+	 Miscops.pr_move_location pr_ident id2)
+  | TacRename l ->
+      hov 1
+        (str "rename" ++ brk (1,1) ++
+         prlist_with_sep
+	   (fun () -> str "," ++ brk (1,1))
+	   (fun (i1,i2) ->
+	      pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2)
+	   l)
+  | TacRevert l ->
+      hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l)
+
+  (* Constructors *)
+  | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
+  | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
+  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_comma pr_bindings l)
+  | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
+  | TacAnyConstructor (ev,Some t) ->
+      hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
+  | TacAnyConstructor (ev,None) as t -> pr_atom0 t
+  | TacConstructor (ev,n,l) ->
+      hov 1 (str (with_evars ev "constructor") ++
+             pr_or_var pr_intarg n ++ pr_bindings l)
+
+  (* Conversion *)
+  | TacReduce (r,h) ->
+      hov 1 (pr_red_expr r ++
+             pr_clauses (Some true) pr_ident h)
+  | TacChange (op,c,h) ->
+      hov 1 (str "change" ++ brk (1,1) ++
+      (match op with
+          None -> mt()
+        | Some p -> pr_pat p ++ spc () ++ str "with ") ++
+      pr_constr c ++ pr_clauses (Some true) pr_ident h)
+
+  (* Equivalence relations *)
+  | TacReflexivity as x -> pr_atom0 x
+  | TacSymmetry cls -> str "symmetry " ++ pr_clauses (Some true) pr_ident cls
+  | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
+  | TacTransitivity None -> str "etransitivity"
+
+  (* Equality and inversion *)
+  | TacRewrite (ev,l,cl,by) ->
+      hov 1 (str (with_evars ev "rewrite") ++
+	     prlist_with_sep
+	     (fun () -> str ","++spc())
+	     (fun (b,m,c) ->
+		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
+	     l
+	     ++ pr_clauses (Some true) pr_ident cl
+	     ++	(match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
+  | TacInversion (DepInversion (k,c,ids),hyp) ->
+      hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
+      pr_quantified_hypothesis hyp ++
+      pr_with_inversion_names ids ++ pr_with_constr pr_constr c)
+  | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+      hov 1 (pr_induction_kind k ++ spc () ++
+      pr_quantified_hypothesis hyp ++
+      pr_with_inversion_names ids ++ pr_simple_hyp_clause pr_ident cl)
+  | TacInversion (InversionUsing (c,cl),hyp) ->
+      hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
+      spc () ++ str "using" ++ spc () ++ pr_constr c ++
+      pr_simple_hyp_clause pr_ident cl)
+
+in
+
+let rec pr_tac inherited tac =
+  let (strm,prec) = match tac with
+  | TacAbstract (t,None) ->
+      str "abstract " ++ pr_tac (labstract,L) t, labstract
+  | TacAbstract (t,Some s) ->
+      hov 0
+       (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++
+        str "using " ++ pr_id s),
+      labstract
+  | TacLetIn (recflag,llc,u) ->
+      let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
+      v 0
+       (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
+       fnl () ++ pr_tac (llet,E) u),
+      llet
+  | TacMatch (lz,t,lrul) ->
+      hov 0 (pr_lazy lz ++ str "match " ++ pr_tac ltop t ++ str " with"
+        ++ prlist
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule true (pr_tac ltop) pr_lpat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
+  | TacMatchGoal (lz,lr,lrul) ->
+      hov 0 (pr_lazy lz ++
+	str (if lr then "match reverse goal with" else "match goal with")
+	++ prlist
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule false (pr_tac ltop) pr_lpat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
+  | TacFun (lvar,body) ->
+      hov 2 (str "fun" ++
+        prlist pr_funvar lvar ++ str " =>" ++ spc () ++
+        pr_tac (lfun,E) body),
+      lfun
+  | TacThens (t,tl) ->
+      hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
+             pr_seq_body (pr_tac ltop) tl),
+      lseq
+  | TacThen (t1,[||],t2,[||]) ->
+      hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+             pr_tac (lseq,L) t2),
+      lseq
+  | TacThen (t1,tf,t2,tl) ->
+      hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+             pr_then_gen (pr_tac ltop) tf t2 tl),
+      lseq
+  | TacTry t ->
+      hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
+      ltactical
+  | TacDo (n,t) ->
+      hov 1 (str "do " ++ pr_or_var int n ++ spc () ++
+             pr_tac (ltactical,E) t),
+      ltactical
+  | TacTimeout (n,t) ->
+      hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++
+             pr_tac (ltactical,E) t),
+      ltactical
+  | TacRepeat t ->
+      hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
+      ltactical
+  | TacProgress t ->
+      hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
+      ltactical
+  | TacInfo t ->
+      hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
+      linfo
+  | TacOrelse (t1,t2) ->
+      hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+             pr_tac (lorelse,E) t2),
+      lorelse
+  | TacFail (n,l) ->
+      hov 1 (str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+      prlist (pr_arg (pr_message_token pr_ident)) l), latom
+  | TacFirst tl ->
+      str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+  | TacSolve tl ->
+      str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+  | TacComplete t ->
+      str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete
+  | TacId l ->
+      str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
+  | TacAtom (loc,TacAlias (_,s,l,_)) ->
+      pr_with_comments loc
+        (pr_extend (level_of inherited) s (List.map snd l)),
+      latom
+  | TacAtom (loc,t) ->
+      pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+  | TacArg(_,Tacexp e) -> pr_tac_level (latom,E) e, latom
+  | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
+      str "constr:" ++ pr_constr c, latom
+  | TacArg(_,ConstrMayEval c) ->
+      pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c, leval
+  | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
+  | TacArg(_,Integer n) -> int n, latom
+  | TacArg(_,TacCall(loc,f,[])) -> pr_ref f, latom
+  | TacArg(_,TacCall(loc,f,l)) ->
+      pr_with_comments loc
+        (hov 1 (pr_ref f ++ spc () ++
+         prlist_with_sep spc pr_tacarg l)),
+      lcall
+  | TacArg (_,a) -> pr_tacarg a, latom
+  in
+  if prec_less prec inherited then strm
+  else str"(" ++ strm ++ str")"
+
+and pr_tacarg = function
+  | TacDynamic (loc,t) ->
+      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+  | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
+  | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
+  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
+  | TacVoid -> str "()"
+  | Reference r -> pr_ref r
+  | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c
+  | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
+  | TacExternal (_,com,req,la) ->
+      str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
+      spc() ++ prlist_with_sep spc pr_tacarg la
+  | (TacCall _|Tacexp _|Integer _) as a ->
+      str "ltac:" ++ pr_tac (latom,E) (TacArg (dummy_loc,a))
+
+in (pr_tac, pr_match_rule)
+
+let strip_prod_binders_glob_constr n (ty,_) =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, (ty,None)) else
+      match ty with
+          Glob_term.GProd(loc,na,Explicit,a,b) ->
+            strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let strip_prod_binders_constr n ty =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, ty) else
+      match Term.kind_of_term ty with
+          Term.Prod(na,a,b) ->
+            strip_ty (([dummy_loc,na],a)::acc) (n-1) b
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let drop_env f _env = f
+
+let pr_constr_or_lconstr_pattern_expr b =
+  if b then pr_lconstr_pattern_expr else pr_constr_pattern_expr
+
+let rec raw_printers =
+    (pr_raw_tactic_level,
+     drop_env pr_constr_expr,
+     drop_env pr_lconstr_expr,
+     pr_constr_or_lconstr_pattern_expr,
+     drop_env (pr_or_by_notation pr_reference),
+     drop_env (pr_or_by_notation pr_reference),
+     pr_reference,
+     pr_or_metaid pr_lident,
+     pr_raw_extend,
+     strip_prod_binders_expr)
+
+and pr_raw_tactic_level env n (t:raw_tactic_expr) =
+  fst (make_pr_tac raw_printers env) n t
+
+let pr_and_constr_expr pr (c,_) = pr c
+
+let pr_pat_and_constr_expr b (c,_) =
+  pr_and_constr_expr ((if b then pr_lglob_constr_env else pr_glob_constr_env)
+    (Global.env())) c
+
+let rec glob_printers =
+    (pr_glob_tactic_level,
+     (fun env -> pr_and_constr_expr (pr_glob_constr_env env)),
+     (fun env -> pr_and_constr_expr (pr_lglob_constr_env env)),
+     pr_pat_and_constr_expr,
+     (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
+     (fun env -> pr_or_var (pr_inductive env)),
+     pr_ltac_or_var (pr_located pr_ltac_constant),
+     pr_lident,
+     pr_glob_extend,
+     strip_prod_binders_glob_constr)
+
+and pr_glob_tactic_level env n (t:glob_tactic_expr) =
+  fst (make_pr_tac glob_printers env) n t
+
+let pr_constr_or_lconstr_pattern b =
+  if b then pr_lconstr_pattern else pr_constr_pattern
+
+let typed_printers =
+    (pr_glob_tactic_level,
+     pr_constr_env,
+     pr_lconstr_env,
+     pr_constr_or_lconstr_pattern,
+     pr_evaluable_reference_env,
+     pr_inductive,
+     pr_ltac_constant,
+     pr_id,
+     pr_extend,
+     strip_prod_binders_constr)
+
+let pr_tactic_level env = fst (make_pr_tac typed_printers env)
+
+let pr_raw_tactic env = pr_raw_tactic_level env ltop
+let pr_glob_tactic env = pr_glob_tactic_level env ltop
+let pr_tactic env = pr_tactic_level env ltop
+
+let _ = Tactic_debug.set_tactic_printer
+  (fun x -> pr_glob_tactic (Global.env()) x)
+
+let _ = Tactic_debug.set_match_pattern_printer
+  (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp)
+
+let _ = Tactic_debug.set_match_rule_printer
+  (fun rl ->
+    pr_match_rule false (pr_glob_tactic (Global.env()))
+      (fun (_,p) -> pr_constr_pattern p) rl)
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
new file mode 100644
index 000000000..58b45152c
--- /dev/null
+++ b/printing/pptactic.mli
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Genarg
+open Constrexpr
+open Tacexpr
+open Proof_type
+open Ppextend
+open Environ
+open Pattern
+open Misctypes
+
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
+val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+
+type 'a raw_extra_genarg_printer =
+    (constr_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) ->
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+type 'a glob_extra_genarg_printer =
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (glob_constr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+type 'a extra_genarg_printer =
+    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+  (** if the boolean is false then the extension applies only to old syntax *)
+val declare_extra_genarg_pprule :
+  ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) ->
+  ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
+  ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit
+
+type grammar_terminals = string option list
+
+  (** if the boolean is false then the extension applies only to old syntax *)
+val declare_extra_tactic_pprule :
+  string * argument_type list * (int * grammar_terminals) -> unit
+
+val exists_extra_tactic_pprule : string -> argument_type list -> bool
+
+val pr_raw_generic :
+  (constr_expr -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
+    std_ppcmds
+
+val pr_raw_extend:
+  (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
+  (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) -> int ->
+    string -> raw_generic_argument list -> std_ppcmds
+
+val pr_glob_extend:
+  (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
+  (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+  (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
+    string -> glob_generic_argument list -> std_ppcmds
+
+val pr_extend :
+  (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
+  (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+  (constr_pattern -> std_ppcmds) -> int ->
+    string -> typed_generic_argument list -> std_ppcmds
+
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
+
+val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
+
+val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds
+
+val pr_hintbases : string list option -> std_ppcmds
+
+val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+val pr_bindings :
+  ('constr -> std_ppcmds) ->
+  ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
new file mode 100644
index 000000000..9a8bf3c38
--- /dev/null
+++ b/printing/ppvernac.ml
@@ -0,0 +1,967 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Nameops
+open Nametab
+open Compat
+open Errors
+open Util
+open Extend
+open Vernacexpr
+open Ppconstr
+open Pptactic
+open Glob_term
+open Genarg
+open Libnames
+open Ppextend
+open Constrexpr
+open Constrexpr_ops
+open Decl_kinds
+open Tacinterp
+open Declaremods
+
+let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+
+let pr_lident (loc,id) =
+  if loc <> dummy_loc then
+    let (b,_) = unloc loc in
+    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+  else pr_id id
+
+let string_of_fqid fqid =
+ String.concat "." (List.map string_of_id fqid)
+
+let pr_fqid fqid = str (string_of_fqid fqid)
+
+let pr_lfqid (loc,fqid) =
+  if loc <> dummy_loc then
+   let (b,_) = unloc loc in
+    pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
+  else
+   pr_fqid fqid
+
+let pr_lname = function
+    (loc,Name id) -> pr_lident (loc,id)
+  | lna -> pr_located pr_name lna
+
+let pr_smart_global = pr_or_by_notation pr_reference
+
+let pr_ltac_ref = Libnames.pr_reference
+
+let pr_module = Libnames.pr_reference
+
+let pr_import_module = Libnames.pr_reference
+
+let sep_end () = str"."
+
+(* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
+
+let pr_raw_tactic_env l env t =
+  pr_glob_tactic env (Tacinterp.glob_tactic_env l env t)
+
+let pr_gen env t =
+  pr_raw_generic
+    pr_constr_expr
+    pr_lconstr_expr
+    (pr_raw_tactic_level env) pr_constr_expr pr_reference t
+
+let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
+
+let rec extract_signature = function
+  | [] -> []
+  | Egramml.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
+  | _::l -> extract_signature l
+
+let rec match_vernac_rule tys = function
+    [] -> raise Not_found
+  | pargs::rls ->
+      if extract_signature pargs = tys then pargs
+      else match_vernac_rule tys rls
+
+let sep = fun _ -> spc()
+let sep_v2 = fun _ -> str"," ++ spc()
+
+let pr_ne_sep sep pr = function
+    [] -> mt()
+  | l -> sep() ++ pr l
+
+let pr_set_entry_type = function
+  | ETName -> str"ident"
+  | ETReference -> str"global"
+  | ETPattern -> str"pattern"
+  | ETConstr _ -> str"constr"
+  | ETOther (_,e) -> str e
+  | ETBigint -> str "bigint"
+  | ETBinder true -> str "binder"
+  | ETBinder false -> str "closed binder"
+  | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
+
+let strip_meta id =
+  let s = string_of_id id in
+  if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+  else id
+
+let pr_production_item = function
+  | TacNonTerm (loc,nt,Some (p,sep)) ->
+      let pp_sep = if sep <> "" then str "," ++ quote (str sep) else mt () in
+      str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
+  | TacNonTerm (loc,nt,None) -> str nt
+  | TacTerm s -> qs s
+
+let pr_comment pr_c = function
+  | CommentConstr c -> pr_c c
+  | CommentString s -> qs s
+  | CommentInt n -> int n
+
+let pr_in_out_modules = function
+  | SearchInside l -> spc() ++ str"inside" ++ spc() ++ prlist_with_sep sep pr_module l
+  | SearchOutside [] -> mt()
+  | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l
+
+let pr_search_about (b,c) =
+  (if b then str "-" else mt()) ++
+  match c with
+  | SearchSubPattern p -> pr_constr_pattern_expr p
+  | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+let pr_search a b pr_p = match a with
+  | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+  | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
+
+let pr_locality_full = function
+  | None -> mt ()
+  | Some true -> str "Local" ++ spc ()
+  | Some false -> str "Global "++ spc ()
+
+let pr_locality local = if local then str "Local" ++ spc () else mt ()
+let pr_non_locality local = if local then mt () else str "Global" ++ spc ()
+let pr_section_locality local =
+  if Lib.sections_are_opened () && not local then str "Global "
+  else if not (Lib.sections_are_opened ()) && local then str "Local "
+  else mt ()
+
+let pr_explanation (e,b,f) =
+  let a = match e with
+  | ExplByPos (n,_) -> anomaly "No more supported"
+  | ExplByName id -> pr_id id in
+  let a = if f then str"!" ++ a else a in
+    if b then str "[" ++ a ++ str "]" else a
+
+let pr_option_ref_value = function
+  | QualidRefValue id -> pr_reference id
+  | StringRefValue s -> qs s
+
+let pr_printoption table b =
+  prlist_with_sep spc str table ++
+  pr_opt (prlist_with_sep sep pr_option_ref_value) b
+
+let pr_set_option a b =
+  let pr_opt_value = function
+    | IntValue None -> assert false
+    (* This should not happen because of the grammar *)
+    | IntValue (Some n) -> spc() ++ int n
+    | StringValue s -> spc() ++ str s
+    | BoolValue b -> mt()
+  in pr_printoption a None ++ pr_opt_value b
+
+let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)"
+
+let pr_destruct_location = function
+  | Tacexpr.ConclLocation ()  -> str"Conclusion"
+  | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis"
+
+let pr_opt_hintbases l = match l with
+  | [] -> mt()
+  | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
+
+let pr_hints local db h pr_c pr_pat =
+  let opth = pr_opt_hintbases db  in
+  let pph =
+    match h with
+    | HintsResolve l ->
+        str "Resolve " ++ prlist_with_sep sep
+	  (fun (pri, _, c) -> pr_c c ++
+	    match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+	  l
+    | HintsImmediate l ->
+        str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
+    | HintsUnfold l ->
+        str "Unfold " ++ prlist_with_sep sep pr_reference l
+    | HintsTransparency (l, b) ->
+        str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep
+	  pr_reference l
+    | HintsConstructors c ->
+        str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
+    | HintsExtern (n,c,tac) ->
+	let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+          str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+          spc() ++ pr_raw_tactic tac
+  in
+  hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
+
+let pr_with_declaration pr_c = function
+  | CWith_Definition (id,c) ->
+      let p = pr_c c in
+      str"Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p
+  | CWith_Module (id,qid) ->
+      str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
+      pr_located pr_qualid qid
+
+let rec pr_module_ast pr_c = function
+  | CMident qid -> spc () ++ pr_located pr_qualid qid
+  | CMwith (_,mty,decl) ->
+      let m = pr_module_ast pr_c mty in
+      let p = pr_with_declaration pr_c decl in
+      m ++ spc() ++ str"with" ++ spc() ++ p
+  | CMapply (_,me1,(CMident _ as me2)) ->
+      pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2
+  | CMapply (_,me1,me2) ->
+      pr_module_ast pr_c me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
+
+let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
+  let sep () = if scl=[] then mt () else str "," in
+  if ann = DefaultInline && scl = [] then mt ()
+  else
+    str " [" ++
+    (match ann with
+      | DefaultInline -> mt ()
+      | NoInline -> str "no inline" ++ sep ()
+      | InlineAt i -> str "inline at level " ++ int i ++ sep ()) ++
+    prlist_with_sep (fun () -> str ", ")
+      (fun (sc1,sc2) -> str ("scope "^sc1^" to "^sc2)) scl ++
+    str "]"
+
+let pr_module_ast_inl pr_c (mast,ann) =
+  pr_module_ast pr_c mast ++ pr_annot ann
+
+let pr_of_module_type prc = function
+  | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
+  | Check mtys ->
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl prc m) mtys
+
+let pr_require_token = function
+  | Some true -> str "Export "
+  | Some false -> str "Import "
+  | None -> mt()
+
+let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
+  let m = pr_module_ast pr_c mty in
+  (* Update the Nametab for interpreting the body of module/modtype *)
+  let lib_dir = Lib.library_dp() in
+  List.iter (fun (_,id) ->
+    Declaremods.process_module_bindings [id]
+      [make_mbid lib_dir id,
+       (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
+  (* Builds the stream *)
+  spc() ++
+  hov 1 (str"(" ++ pr_require_token export ++
+   prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+
+let pr_module_binders l pr_c =
+  (* Effet de bord complexe pour garantir la declaration des noms des
+  modules parametres dans la Nametab des l'appel de pr_module_binders
+  malgre l'aspect paresseux des streams *)
+  let ml = List.map (pr_module_vardecls pr_c) l in
+  prlist (fun id -> id) ml
+
+let pr_module_binders_list l pr_c = pr_module_binders l pr_c
+
+let pr_type_option pr_c = function
+  | CHole (loc, k) -> mt()
+  | _ as c -> brk(0,2) ++ str":" ++ pr_c c
+
+let pr_decl_notation prc ((loc,ntn),c,scopt) =
+  fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++
+  pr_opt (fun sc -> str ": " ++ str sc) scopt
+
+let pr_binders_arg =
+  pr_ne_sep spc pr_binders
+
+let pr_and_type_binders_arg bl =
+  pr_binders_arg bl
+
+let pr_onescheme (idop,schem) =
+  match schem with
+  | InductionScheme (dep,ind,s) ->
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc ()
+    ) ++
+    hov 0 ((if dep then str"Induction for" else str"Minimality for")
+    ++ spc() ++ pr_smart_global ind) ++ spc() ++
+    hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s)
+  | CaseScheme (dep,ind,s) ->
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc ()
+    ) ++
+    hov 0 ((if dep then str"Elimination for" else str"Case for")
+    ++ spc() ++ pr_smart_global ind) ++ spc() ++
+    hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s)
+  | EqualityScheme ind ->
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc()
+    ) ++
+    hov 0 (str"Equality for")
+    ++ spc() ++ pr_smart_global ind
+
+let begin_of_inductive = function
+    [] -> 0
+  | (_,((loc,_),_))::_ -> fst (unloc loc)
+
+let pr_class_rawexpr = function
+  | FunClass -> str"Funclass"
+  | SortClass -> str"Sortclass"
+  | RefClass qid -> pr_smart_global qid
+
+let pr_assumption_token many = function
+  | (Local,Logical) ->
+      str (if many then "Hypotheses" else "Hypothesis")
+  | (Local,Definitional) ->
+      str (if many then "Variables" else "Variable")
+  | (Global,Logical) ->
+      str (if many then "Axioms" else "Axiom")
+  | (Global,Definitional) ->
+      str (if many then "Parameters" else "Parameter")
+  | (Global,Conjectural) -> str"Conjecture"
+  | (Local,Conjectural) ->
+      anomaly "Don't know how to beautify a local conjecture"
+
+let pr_params pr_c (xl,(c,t)) =
+  hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
+         (if c then str":>" else str":" ++
+         spc() ++ pr_c t))
+
+let rec factorize = function
+  | [] -> []
+  | (c,(idl,t))::l ->
+      match factorize l with
+	| (xl,t')::l' when t' = (c,t) -> (idl@xl,t')::l'
+	| l' -> (idl,(c,t))::l'
+
+let pr_ne_params_list pr_c l =
+  match factorize l with
+    | [p] -> pr_params pr_c p
+    | l ->
+	prlist_with_sep spc
+          (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+(*
+  prlist_with_sep pr_semicolon (pr_params pr_c)
+*)
+
+let pr_thm_token k = str (Kindops.string_of_theorem_kind k)
+
+let pr_syntax_modifier = function
+  | SetItemLevel (l,NextLevel) ->
+      prlist_with_sep sep_v2 str l ++
+      spc() ++ str"at next level"
+  | SetItemLevel (l,NumLevel n) ->
+      prlist_with_sep sep_v2 str l ++
+      spc() ++ str"at level" ++ spc() ++ int n
+  | SetLevel n -> str"at level" ++ spc() ++ int n
+  | SetAssoc LeftA -> str"left associativity"
+  | SetAssoc RightA -> str"right associativity"
+  | SetAssoc NonA -> str"no associativity"
+  | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+  | SetOnlyParsing -> str"only parsing"
+  | SetFormat s -> str"format " ++ pr_located qs s
+
+let pr_syntax_modifiers = function
+  | [] -> mt()
+  | l -> spc() ++
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+
+let print_level n =
+  if n <> 0 then str " (at level " ++ int n ++ str ")" else mt ()
+
+let pr_grammar_tactic_rule n (_,pil,t) =
+  hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++
+    hov 0 (prlist_with_sep sep pr_production_item pil ++
+    spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
+
+let pr_statement head (id,(bl,c,guard)) =
+  assert (id<>None);
+  hov 1
+    (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+    (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+    pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
+    str":" ++ pr_spc_lconstr c)
+
+(**************************************)
+(* Pretty printer for vernac commands *)
+(**************************************)
+let make_pr_vernac pr_constr pr_lconstr =
+
+let pr_constrarg c = spc () ++ pr_constr c in
+let pr_lconstrarg c = spc () ++ pr_lconstr c in
+let pr_intarg n = spc () ++ int n in
+let pr_oc = function
+    None -> str" :"
+  | Some true -> str" :>"
+  | Some false -> str" :>>"
+in
+let pr_record_field ((x, pri), ntn) =
+  let prx = match x with
+    | (oc,AssumExpr (id,t)) ->
+	hov 1 (pr_lname id ++
+	       pr_oc oc ++ spc() ++
+	       pr_lconstr_expr t)
+    | (oc,DefExpr(id,b,opt)) -> (match opt with
+      | Some t ->
+          hov 1 (pr_lname id ++
+                 pr_oc oc ++ spc() ++
+                 pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+      | None ->
+          hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+                    pr_lconstr b)) in
+  let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
+    prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+in
+let pr_record_decl b c fs =
+    pr_opt pr_lident c ++ str"{"  ++
+    hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+in
+
+let rec pr_vernac = function
+
+  (* Proof management *)
+  | VernacAbortAll -> str "Abort All"
+  | VernacRestart -> str"Restart"
+  | VernacUnfocus -> str"Unfocus"
+  | VernacUnfocused -> str"Unfocused"
+  | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
+  | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
+  | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
+  | VernacBacktrack (i,j,k) ->
+      str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
+  | VernacFocus i -> str"Focus" ++ pr_opt int i
+  | VernacShow s ->
+      let pr_goal_reference = function
+        | OpenSubgoals -> mt ()
+        | NthGoal n -> spc () ++ int n
+        | GoalId n -> spc () ++ str n in
+      let pr_showable = function
+	| ShowGoal n -> str"Show" ++ pr_goal_reference n
+	| ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n
+	| ShowProof -> str"Show Proof"
+	| ShowNode -> str"Show Node"
+	| ShowScript -> str"Show Script"
+	| ShowExistentials -> str"Show Existentials"
+	| ShowTree -> str"Show Tree"
+	| ShowProofNames -> str"Show Conjectures"
+	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
+	| ShowMatch id -> str"Show Match " ++ pr_lident id
+	| ShowThesis -> str "Show Thesis"
+      in pr_showable s
+  | VernacCheckGuard -> str"Guarded"
+
+  (* Resetting *)
+  | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
+  | VernacResetInitial -> str"Reset Initial"
+  | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
+  | VernacBackTo i -> str"BackTo" ++ pr_intarg i
+
+  (* State management *)
+  | VernacWriteState s -> str"Write State" ++ spc () ++ qs s
+  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
+
+  (* Control *)
+  | VernacList l ->
+      hov 2 (str"[" ++ spc() ++
+             prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l
+             ++ spc() ++ str"]")
+  | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
+  ++ spc()) else spc()  ++ qs s
+  | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
+  | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v
+  | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
+
+  (* Syntax *)
+  | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
+  | VernacOpenCloseScope (local,opening,sc) ->
+      pr_section_locality local ++
+      str (if opening then "Open " else "Close ") ++
+      str "Scope" ++ spc() ++ str sc
+  | VernacDelimiters (sc,key) ->
+      str"Delimit Scope" ++ spc () ++ str sc ++
+      spc() ++ str "with " ++ str key
+  | VernacBindScope (sc,cll) ->
+      str"Bind Scope" ++ spc () ++ str sc ++
+      spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
+  | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
+      |	None -> str"_"
+      |	Some sc -> str sc in
+    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++
+    pr_smart_global q
+    ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
+  | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
+      hov 0 (hov 0 (pr_locality local ++ str"Infix "
+      ++ qs s ++ str " :=" ++ pr_constrarg q) ++
+      pr_syntax_modifiers mv ++
+      (match sn with
+    | None -> mt()
+    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+  | VernacNotation (local,c,((_,s),l),opt) ->
+      let ps =
+	let n = String.length s in
+	if n > 2 & s.[0] = '\'' & s.[n-1] = '\''
+	then
+          let s' = String.sub s 1 (n-2) in
+          if String.contains s' '\'' then qs s else str s'
+	else qs s in
+      hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++
+      str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
+      (match opt with
+        | None -> mt()
+        | Some sc -> str" :" ++ spc() ++ str sc))
+  | VernacSyntaxExtension (local,(s,l)) ->
+      pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
+      pr_syntax_modifiers l
+
+  (* Gallina *)
+  | VernacDefinition (d,id,b,f) -> (* A verifier... *)
+      let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
+      let pr_reduce = function
+        | None -> mt()
+        | Some r ->
+            str"Eval" ++ spc() ++
+            pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+            str" in" ++ spc() in
+      let pr_def_body = function
+        | DefineBody (bl,red,body,d) ->
+            let ty = match d with
+              | None -> mt()
+              | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
+	    in
+            (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+        | ProveBody (bl,t) ->
+            (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
+      let (binds,typ,c) = pr_def_body b in
+      hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
+      (match c with
+        | None -> mt()
+        | Some cc -> str" :=" ++ spc() ++ cc))
+
+  | VernacStartTheoremProof (ki,l,_,_) ->
+      hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
+             prlist (pr_statement (spc () ++ str "with")) (List.tl l))
+
+  | VernacEndProof Admitted -> str"Admitted"
+  | VernacEndProof (Proved (opac,o)) -> (match o with
+    | None -> if opac then str"Qed" else str"Defined"
+    | Some (id,th) -> (match th with
+      |	None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id
+      |	Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id))
+  | VernacExactProof c ->
+      hov 2 (str"Proof" ++ pr_lconstrarg c)
+  | VernacAssumption (stre,_,l) ->
+      let n = List.length (List.flatten (List.map fst (List.map snd l))) in
+      hov 2
+        (pr_assumption_token (n > 1) stre ++ spc() ++
+	 pr_ne_params_list pr_lconstr_expr l)
+  | VernacInductive (f,i,l) ->
+
+      let pr_constructor (coe,(id,c)) =
+        hov 2 (pr_lident id ++ str" " ++
+               (if coe then str":>" else str":") ++
+                pr_spc_lconstr c) in
+      let pr_constructor_list b l = match l with
+        | Constructors [] -> mt()
+        | Constructors l ->
+            pr_com_at (begin_of_inductive l) ++
+            fnl() ++
+            str (if List.length l = 1 then "   " else " | ") ++
+            prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+       | RecordDecl (c,fs) ->
+	    spc() ++
+	    pr_record_decl b c fs in
+      let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+	hov 0 (
+	    str key ++ spc() ++
+	      (if i then str"Infer " else str"") ++
+              (if coe then str"> " else str"") ++ pr_lident id ++
+              pr_and_type_binders_arg indpar ++ spc() ++
+	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+	      str" :=") ++ pr_constructor_list k lc ++
+	    prlist (pr_decl_notation pr_constr) ntn
+      in
+      let key =
+        let (_,_,_,k,_),_ = List.hd l in
+	match k with Record -> "Record" | Structure -> "Structure"
+	  | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+	  | Class _ -> "Class" in
+      hov 1 (pr_oneind key (List.hd l)) ++
+      (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+
+
+  | VernacFixpoint recs ->
+      let pr_onerec = function
+        | ((loc,id),ro,bl,type_,def),ntn ->
+            let annot = pr_guard_annot pr_lconstr_expr bl ro in
+            pr_id id ++ pr_binders_arg bl ++ annot
+            ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
+            ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+	    prlist (pr_decl_notation pr_constr) ntn
+      in
+      hov 0 (str "Fixpoint" ++ spc() ++
+        prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
+
+  | VernacCoFixpoint corecs ->
+      let pr_onecorec (((loc,id),bl,c,def),ntn) =
+        pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+        spc() ++ pr_lconstr_expr c ++
+        pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
+	prlist (pr_decl_notation pr_constr) ntn
+      in
+      hov 0 (str "CoFixpoint" ++ spc() ++
+      prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
+  | VernacScheme l ->
+      hov 2 (str"Scheme" ++ spc() ++
+             prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
+  | VernacCombinedScheme (id, l) ->
+      hov 2 (str"Combined Scheme" ++ spc() ++
+	       pr_lident id ++ spc() ++ str"from" ++ spc() ++
+	       prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+
+
+  (* Gallina extensions *)
+  | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
+  | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
+  | VernacRequire (exp, l) -> hov 2
+      (str "Require" ++ spc() ++ pr_require_token exp ++
+      prlist_with_sep sep pr_module l)
+  | VernacImport (f,l) ->
+      (if f then str"Export" else str"Import") ++ spc() ++
+      prlist_with_sep sep pr_import_module l
+  | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
+  | VernacCoercion (s,id,c1,c2) ->
+      hov 1 (
+	str"Coercion" ++ (match s with | Local -> spc() ++
+	  str"Local" ++ spc() | Global -> spc()) ++
+	pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+	spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+  | VernacIdentityCoercion (s,id,c1,c2) ->
+      hov 1 (
+	str"Identity Coercion" ++ (match s with | Local -> spc() ++
+	  str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++
+	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+	spc() ++ pr_class_rawexpr c2)
+
+ | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
+     hov 1 (
+       pr_non_locality (not glob) ++
+       (if abst then str"Declare " else mt ()) ++
+       str"Instance" ++
+       (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
+	Anonymous -> mt ()) ++
+       pr_and_type_binders_arg sup ++
+       str":" ++ spc () ++
+       pr_constr_expr cl ++ spc () ++
+	 (match props with
+	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p
+	  | None -> mt()))
+
+ | VernacContext l ->
+     hov 1 (
+       str"Context" ++ spc () ++ pr_and_type_binders_arg l)
+
+
+ | VernacDeclareInstances (glob, ids) ->
+     hov 1 (pr_non_locality (not glob) ++
+               str"Existing" ++ spc () ++ str(plural (List.length ids) "Instance") ++
+               spc () ++ prlist_with_sep spc pr_reference ids)
+
+ | VernacDeclareClass id ->
+     hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
+
+  (* Modules and Module Types *)
+  | VernacDefineModule (export,m,bl,tys,bd) ->
+      let b = pr_module_binders_list bl pr_lconstr in
+      hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
+               pr_lident m ++ b ++
+               pr_of_module_type pr_lconstr tys ++
+	       (if bd = [] then mt () else str ":= ") ++
+	       prlist_with_sep (fun () -> str " <+ ")
+	        (pr_module_ast_inl pr_lconstr) bd)
+  | VernacDeclareModule (export,id,bl,m1) ->
+      let b = pr_module_binders_list bl pr_lconstr in
+	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
+             pr_lident id ++ b ++
+             pr_module_ast_inl pr_lconstr m1)
+  | VernacDeclareModuleType (id,bl,tyl,m) ->
+      let b = pr_module_binders_list bl pr_lconstr in
+      let pr_mt = pr_module_ast_inl pr_lconstr in
+	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
+		 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
+		 (if m = [] then mt () else str ":= ") ++
+		 prlist_with_sep (fun () -> str " <+ ") pr_mt m)
+  | VernacInclude (mexprs) ->
+      let pr_m = pr_module_ast_inl pr_lconstr in
+      hov 2 (str"Include " ++
+	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
+  (* Solving *)
+  | VernacSolve (i,tac,deftac) ->
+      (if i = 1 then mt() else int i ++ str ": ") ++
+      pr_raw_tactic tac
+      ++ (try if deftac then str ".." else mt ()
+      with UserError _|Loc.Exc_located _ -> mt())
+
+  | VernacSolveExistential (i,c) ->
+      str"Existential " ++ int i ++ pr_lconstrarg c
+
+  (* Auxiliary file and library management *)
+  | VernacRequireFrom (exp, f) -> hov 2
+      (str "Require" ++ spc() ++ pr_require_token exp ++ qs f)
+  | VernacAddLoadPath (fl,s,d) -> hov 2
+      (str"Add" ++
+       (if fl then str" Rec " else spc()) ++
+       str"LoadPath" ++ spc() ++ qs s ++
+       (match d with
+         | None -> mt()
+         | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir))
+  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
+  | VernacAddMLPath (fl,s) ->
+      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
+  | VernacDeclareMLModule (local, l) ->
+      pr_locality local ++
+      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qs s
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition (local,rc,l) ->
+      let pr_tac_body (id, redef, body) =
+        let idl, body =
+          match body with
+	    | Tacexpr.TacFun (idl,b) -> idl,b
+            | _ -> [], body in
+        pr_ltac_ref id ++
+	prlist (function None -> str " _"
+                       | Some id -> spc () ++ pr_id id) idl
+	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
+	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
+        pr_raw_tactic_env
+	  (idl @ List.map coerce_reference_to_id
+	    (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
+	  (Global.env())
+	  body in
+      hov 1
+        (pr_locality local ++ str "Ltac " ++
+        prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
+  | VernacCreateHintDb (local,dbname,b) ->
+      hov 1 (pr_locality local ++ str "Create HintDb " ++
+		str dbname ++ (if b then str" discriminated" else mt ()))
+  | VernacRemoveHints (local, dbnames, ids) ->
+      hov 1 (pr_locality local ++ str "Remove Hints " ++
+	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
+	       pr_opt_hintbases dbnames)
+  | VernacHints (local,dbnames,h) ->
+      pr_hints local dbnames h pr_constr pr_constr_pattern_expr
+  | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
+      hov 2
+        (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
+         pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
+  | VernacDeclareImplicits (local,q,[]) ->
+      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
+	pr_smart_global q)
+  | VernacDeclareImplicits (local,q,impls) ->
+      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++
+	spc() ++ pr_smart_global q ++ spc() ++
+	prlist_with_sep spc (fun imps ->
+	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	  impls)
+  | VernacArguments (local, q, impl, nargs, mods) ->
+      hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+        pr_smart_global q ++
+      let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+      let pr_if b x = if b then x else str "" in
+      let pr_br imp max x = match imp, max with
+        | true, false -> str "[" ++ x ++ str "]"
+        | true, true -> str "{" ++ x ++ str "}"
+        | _ -> x in
+      let rec aux n l =
+        match n, l with
+        | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+        | _, [] -> mt()
+        | n, (id,k,s,imp,max) :: tl ->
+            spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+            aux (n-1) tl in
+      prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+      if mods <> [] then str" : " else str"" ++
+      prlist_with_sep (fun () -> str", " ++ spc()) (function
+        | `SimplDontExposeCase -> str "simpl nomatch"
+        | `SimplNeverUnfold -> str "simpl never"
+        | `DefaultImplicits -> str "default implicits"
+        | `Rename -> str "rename"
+        | `ExtraScopes -> str "extra scopes"
+        | `ClearImplicits -> str "clear implicits"
+        | `ClearScopes -> str "clear scopes")
+        mods)
+  | VernacReserve bl ->
+      let n = List.length (List.flatten (List.map fst bl)) in
+      hov 2 (str"Implicit Type" ++
+        str (if n > 1 then "s " else " ") ++
+        pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+  | VernacGeneralizable (local, g) ->
+      hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+		match g with
+		| None -> str "s none"
+		| Some [] -> str "s all"
+		| Some idl ->
+		    str (if List.length idl > 1 then "s " else " ") ++
+		      prlist_with_sep spc pr_lident idl)
+  | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
+      hov 1 (pr_non_locality b ++ str "Transparent" ++
+             spc() ++ prlist_with_sep sep pr_smart_global l)
+  | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
+      hov 1 (pr_non_locality b ++ str "Opaque" ++
+             spc() ++ prlist_with_sep sep pr_smart_global l)
+  | VernacSetOpacity (local,l) ->
+      let pr_lev = function
+          Conv_oracle.Opaque -> str"opaque"
+        | Conv_oracle.Expand -> str"expand"
+        | l when l = Conv_oracle.transparent -> str"transparent"
+        | Conv_oracle.Level n -> int n in
+      let pr_line (l,q) =
+        hov 2 (pr_lev l ++ spc() ++
+               str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
+      hov 1 (pr_locality local ++ str "Strategy" ++ spc() ++
+             hv 0 (prlist_with_sep sep pr_line l))
+  | VernacUnsetOption (l,na) ->
+      hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (l,na,v) ->
+      hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v)
+  | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
+  | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
+  | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
+  | VernacPrintOption na -> hov 2 (str"Test" ++ spc() ++ pr_printoption na None)
+  | VernacCheckMayEval (r,io,c) ->
+      let pr_mayeval r c = match r with
+      | Some r0 ->
+          hov 2 (str"Eval" ++ spc() ++
+          pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
+          spc() ++ str"in" ++ spc () ++ pr_constr c)
+      | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c)
+      in
+      (if io = None then mt() else int (Option.get io) ++ str ": ") ++
+      pr_mayeval r c
+  | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
+  | VernacDeclareReduction (b,s,r) ->
+     pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
+     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
+  | VernacPrint p ->
+      let pr_printable = function
+	| PrintFullContext -> str"Print All"
+	| PrintSectionContext s ->
+            str"Print Section" ++ spc() ++ Libnames.pr_reference s
+	| PrintGrammar ent ->
+            str"Print Grammar" ++ spc() ++ str ent
+	| PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir
+	| PrintModules -> str"Print Modules"
+	| PrintMLLoadPath -> str"Print ML Path"
+	| PrintMLModules -> str"Print ML Modules"
+	| PrintGraph -> str"Print Graph"
+	| PrintClasses -> str"Print Classes"
+	| PrintTypeClasses -> str"Print TypeClasses"
+	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_smart_global qid
+	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_ltac_ref qid
+	| PrintCoercions -> str"Print Coercions"
+	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
+	| PrintCanonicalConversions -> str"Print Canonical Structures"
+	| PrintTables -> str"Print Tables"
+	| PrintHintGoal -> str"Print Hint"
+	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_smart_global qid
+	| PrintHintDb -> str"Print Hint *"
+	| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
+	| PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s
+	| PrintUniverses (b, fopt) -> Printf.ksprintf str "Print %sUniverses" (if b then "Sorted " else "") ++ pr_opt str fopt
+	| PrintName qid -> str"Print" ++ spc()  ++ pr_smart_global qid
+	| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
+	| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
+	| PrintInspect n -> str"Inspect" ++ spc() ++ int n
+	| PrintScopes -> str"Print Scopes"
+	| PrintScope s -> str"Print Scope" ++ spc() ++ str s
+	| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s
+	| PrintAbout qid -> str"About" ++ spc()  ++ pr_smart_global qid
+	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_smart_global qid
+(* spiwack: command printing all the axioms and section variables used in a
+         term *)
+	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+	    ++ spc() ++ pr_smart_global qid
+      in pr_printable p
+  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
+  | VernacLocate loc ->
+      let pr_locate =function
+	| LocateTerm qid -> pr_smart_global qid
+	| LocateFile f -> str"File" ++ spc() ++ qs f
+	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
+	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
+	| LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid
+      in str"Locate" ++ spc() ++ pr_locate loc
+  | VernacComments l ->
+      hov 2
+        (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l)
+  | VernacNop -> mt()
+
+  (* Toplevel control *)
+  | VernacToplevelControl exn -> pr_topcmd exn
+
+  (* For extension *)
+  | VernacExtend (s,c) -> pr_extend s c
+  | VernacProof (None, None) -> str "Proof"
+  | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l
+  | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te
+  | VernacProof (Some te, Some l) ->
+      str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
+      str "with" ++ spc() ++pr_raw_tactic te
+  | VernacProofMode s -> str ("Proof Mode "^s)
+  | VernacBullet b -> begin match b with
+      | Dash -> str"-"
+      | Star -> str"*"
+      | Plus -> str"+"
+  end ++ spc()
+  | VernacSubproof None -> str "{"
+  | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i
+  | VernacEndSubproof -> str "}"
+
+and pr_extend s cl =
+  let pr_arg a =
+    try pr_gen (Global.env()) a
+    with Failure _ -> str ("<error in "^s^">") in
+  try
+    let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in
+    let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+    let start,rl,cl =
+      match rl with
+      | Egramml.GramTerminal s :: rl -> str s, rl, cl
+      | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
+      | [] -> anomaly "Empty entry" in
+    let (pp,_) =
+      List.fold_left
+        (fun (strm,args) pi ->
+          let pp,args = match pi with
+          | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
+          | Egramml.GramTerminal s -> (str s, args) in
+          (strm ++ spc() ++ pp), args)
+        (start,cl) rl in
+    hov 1 pp
+  with Not_found ->
+    hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+in pr_vernac
+
+let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
+
+let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end ()
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
new file mode 100644
index 000000000..91bb19a8c
--- /dev/null
+++ b/printing/ppvernac.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Genarg
+open Vernacexpr
+open Names
+open Nameops
+open Nametab
+open Errors
+open Util
+open Ppconstr
+open Pptactic
+open Glob_term
+open Pcoq
+open Libnames
+open Ppextend
+open Topconstr
+
+val sep_end : unit -> std_ppcmds
+
+(** Prints a vernac expression *)
+val pr_vernac_body : vernac_expr -> std_ppcmds
+
+(** Prints a vernac expression and closes it with a dot. *)
+val pr_vernac : vernac_expr -> std_ppcmds
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
new file mode 100644
index 000000000..7bd41cc22
--- /dev/null
+++ b/printing/prettyp.ml
@@ -0,0 +1,785 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
+ * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
+ *)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Inductive
+open Inductiveops
+open Sign
+open Reduction
+open Environ
+open Declare
+open Impargs
+open Libobject
+open Libnames
+open Globnames
+open Nametab
+open Recordops
+open Misctypes
+open Printer
+open Printmod
+
+type object_pr = {
+  print_inductive           : mutual_inductive -> std_ppcmds;
+  print_constant_with_infos : constant -> std_ppcmds;
+  print_section_variable    : variable -> std_ppcmds;
+  print_syntactic_def       : kernel_name -> std_ppcmds;
+  print_module              : bool -> Names.module_path -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
+  print_named_decl          : identifier * constr option * types -> std_ppcmds;
+  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
+  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
+  print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds;
+}
+
+let gallina_print_module  = print_module
+let gallina_print_modtype = print_modtype
+
+(**************)
+(** Utilities *)
+
+let print_closed_sections = ref false
+
+let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) ++ fnl()
+
+let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l
+
+let blankline = mt() (* add a blank sentence in the list of infos *)
+
+let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
+
+let int_or_no n = if n=0 then str "no" else int n
+
+(*******************)
+(** Basic printing *)
+
+let print_basename sp = pr_global (ConstRef sp)
+
+let print_ref reduce ref =
+  let typ = Global.type_of_global ref in
+  let typ =
+    if reduce then
+      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+      in it_mkProd_or_LetIn ccl ctx
+    else typ in
+  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ)
+
+(********************************)
+(** Printing implicit arguments *)
+
+let conjugate_verb_to_be = function [_] -> "is" | _ -> "are"
+
+let pr_impl_name imp = pr_id (name_of_implicit imp)
+
+let print_impargs_by_name max = function
+  | []  -> []
+  | impls ->
+     [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
+      prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++
+      str (conjugate_verb_to_be impls) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt()))]
+
+let print_one_impargs_list l =
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = list_subtract imps maximps in
+  print_impargs_by_name false nonmaximps @
+  print_impargs_by_name true maximps
+
+let print_impargs_list prefix l =
+  let l = extract_impargs_data l in
+  List.flatten (List.map (fun (cond,imps) ->
+    match cond with
+    | None ->
+	List.map (fun pp -> add_colon prefix ++ pp)
+	  (print_one_impargs_list imps)
+    | Some (n1,n2) ->
+       [v 2 (prlist_with_sep cut (fun x -> x)
+	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
+	   str " applied to " ++
+	   (if n1 = n2 then int_or_no n2 else
+	    if n1 = 0 then str "less than " ++ int n2
+	    else int n1 ++ str " to " ++ int_or_no n2) ++
+	    str (plural n2 " argument") ++ str ":";
+          v 0 (prlist_with_sep cut (fun x -> x)
+	    (if List.exists is_status_implicit imps
+	    then print_one_impargs_list imps
+	    else [str "No implicit arguments"]))])]) l)
+
+let print_renames_list prefix l =
+  if l = [] then [] else
+  [add_colon prefix ++ str "Arguments are renamed to " ++
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+
+let need_expansion impl ref =
+  let typ = Global.type_of_global ref in
+  let ctx = (prod_assum typ) in
+  let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
+  impl <> [] & List.length impl >= nprods &
+    let _,lastimpl = list_chop nprods impl in
+      List.filter is_status_implicit lastimpl <> []
+
+let print_impargs ref =
+  let ref = Smartlocate.smart_global ref in
+  let impl = implicits_of_global ref in
+  let has_impl = impl <> [] in
+  (* Need to reduce since implicits are computed with products flattened *)
+  pr_infos_list
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+       blankline ] @
+    (if has_impl then print_impargs_list (mt()) impl
+     else [str "No implicit arguments"]))
+
+(*********************)
+(** Printing Scopes  *)
+
+let print_argument_scopes prefix = function
+  | [Some sc] ->
+      [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
+  | l when not (List.for_all ((=) None) l) ->
+     [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
+      str "[" ++
+      pr_sequence (function Some sc -> str sc | None -> str "_") l ++
+      str "]")]
+  | _  -> []
+
+(*****************************)
+(** Printing simpl behaviour *)
+
+let print_simpl_behaviour ref =
+  match Tacred.get_simpl_behaviour ref with
+  | None -> []
+  | Some (recargs, nargs, flags) ->
+     let never = List.mem `SimplNeverUnfold flags in
+     let nomatch = List.mem `SimplDontExposeCase flags in
+     let pp_nomatch = spc() ++ if nomatch then
+       str "avoiding to expose match constructs" else str"" in
+     let pp_recargs = spc() ++ str "when the " ++
+       pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (plural (List.length recargs) " argument") ++
+       str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+       str " to a constructor" in
+     let pp_nargs =
+       spc() ++ str "when applied to " ++ int nargs ++
+       str (plural nargs " argument") in
+     [hov 2 (str "The simpl tactic " ++
+     match recargs, nargs, never with
+     | _,_, true -> str "never unfolds " ++ pr_global ref
+     | [], 0, _ -> str "always unfolds " ++ pr_global ref
+     | _::_, n, _ when n < 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | _::_, n, _ when n > List.fold_left max 0 recargs ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++
+        str " and" ++ pp_nargs ++ pp_nomatch
+     | _::_, _, _ ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | [], n, _ when n > 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
+     | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )]
+;;
+
+(*********************)
+(** Printing Opacity *)
+
+type opacity =
+  | FullyOpaque
+  | TransparentMaybeOpacified of Conv_oracle.level
+
+let opacity env = function
+  | VarRef v when pi2 (Environ.lookup_named v env) <> None ->
+      Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v)))
+  | ConstRef cst ->
+      let cb = Environ.lookup_constant cst env in
+      (match cb.const_body with
+	| Undef _ -> None
+	| OpaqueDef _ -> Some FullyOpaque
+	| Def _ -> Some
+          (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst))))
+  | _ -> None
+
+let print_opacity ref =
+  match opacity (Global.env()) ref with
+    | None -> []
+    | Some s ->
+       [pr_global ref ++ str " is " ++
+        str (match s with
+          | FullyOpaque -> "opaque"
+          | TransparentMaybeOpacified Conv_oracle.Opaque ->
+              "basically transparent but considered opaque for reduction"
+          | TransparentMaybeOpacified lev when lev = Conv_oracle.transparent ->
+              "transparent"
+          | TransparentMaybeOpacified (Conv_oracle.Level n) ->
+              "transparent (with expansion weight "^string_of_int n^")"
+          | TransparentMaybeOpacified Conv_oracle.Expand ->
+              "transparent (with minimal expansion weight)")]
+
+(*******************)
+(* *)
+
+let print_name_infos ref =
+  let impls = implicits_of_global ref in
+  let scopes = Notation.find_arguments_scope ref in
+  let renames =
+    try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
+  let type_info_for_implicit =
+    if need_expansion (select_impargs_size 0 impls) ref then
+      (* Need to reduce since implicits are computed with products flattened *)
+      [str "Expanded type for implicit arguments";
+       print_ref true ref; blankline]
+    else
+      [] in
+  type_info_for_implicit @
+  print_renames_list (mt()) renames @
+  print_impargs_list (mt()) impls @
+  print_argument_scopes (mt()) scopes
+
+let print_id_args_data test pr id l =
+  if List.exists test l then
+    pr (str "For " ++ pr_id id) l
+  else
+    []
+
+let print_args_data_of_inductive_ids get test pr sp mipv =
+  List.flatten (Array.to_list (Array.mapi
+    (fun i mip ->
+      print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @
+      List.flatten (Array.to_list (Array.mapi
+	(fun j idc ->
+	  print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1))))
+        mip.mind_consnames)))
+    mipv))
+
+let print_inductive_implicit_args =
+  print_args_data_of_inductive_ids
+    implicits_of_global (fun l -> positions_of_implicits l <> [])
+    print_impargs_list
+
+let print_inductive_renames =
+  print_args_data_of_inductive_ids
+    (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
+    ((<>) Anonymous)
+    print_renames_list
+
+let print_inductive_argument_scopes =
+  print_args_data_of_inductive_ids
+    Notation.find_arguments_scope ((<>) None) print_argument_scopes
+
+(*********************)
+(* "Locate" commands *)
+
+type logical_name =
+  | Term of global_reference
+  | Dir of global_dir_reference
+  | Syntactic of kernel_name
+  | ModuleType of qualid * module_path
+  | Undefined of qualid
+
+let locate_any_name ref =
+  let module N = Nametab in
+  let (loc,qid) = qualid_of_reference ref in
+  try Term (N.locate qid)
+  with Not_found ->
+  try Syntactic (N.locate_syndef qid)
+  with Not_found ->
+  try Dir (N.locate_dir qid)
+  with Not_found ->
+  try ModuleType (qid, N.locate_modtype qid)
+  with Not_found -> Undefined qid
+
+let pr_located_qualid = function
+  | Term ref ->
+      let ref_str = match ref with
+	  ConstRef _ -> "Constant"
+	| IndRef _ -> "Inductive"
+	| ConstructRef _ -> "Constructor"
+	| VarRef _ -> "Variable" in
+      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref)
+  | Syntactic kn ->
+      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
+  | Dir dir ->
+      let s,dir = match dir with
+	| DirOpenModule (dir,_) -> "Open Module", dir
+	| DirOpenModtype (dir,_) -> "Open Module Type", dir
+	| DirOpenSection (dir,_) -> "Open Section", dir
+	| DirModule (dir,_) -> "Module", dir
+	| DirClosedSection dir -> "Closed Section", dir
+      in
+      str s ++ spc () ++ pr_dirpath dir
+  | ModuleType (qid,_) ->
+      str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid)
+  | Undefined qid ->
+      pr_qualid qid ++ spc () ++ str "not a defined object."
+
+let print_located_qualid ref =
+  let (loc,qid) = qualid_of_reference ref in
+  let module N = Nametab in
+  let expand = function
+    | TrueGlobal ref ->
+	Term ref, N.shortest_qualid_of_global Idset.empty ref
+    | SynDef kn ->
+	Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
+  match List.map expand (N.locate_extended_all qid) with
+    | [] ->
+	let (dir,id) = repr_qualid qid in
+	if dir = empty_dirpath then
+	  str "No object of basename " ++ pr_id id
+	else
+	  str "No object of suffix " ++ pr_qualid qid
+    | l ->
+	prlist_with_sep fnl
+	(fun (o,oqid) ->
+	  hov 2 (pr_located_qualid o ++
+	  (if oqid <> qid then
+	    spc() ++ str "(shorter name to refer to it in current context is " ++ pr_qualid oqid ++ str")"
+	  else
+	    mt ()))) l
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Gallina layer                  *****)
+
+let gallina_print_typed_value_in_env env (trm,typ) =
+  (pr_lconstr_env env trm ++ fnl () ++
+     str "     : " ++ pr_ltype_env env typ ++ fnl ())
+
+(* To be improved; the type should be used to provide the types in the
+   abstractions. This should be done recursively inside pr_lconstr, so that
+   the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
+   synthesizes the type nat of the abstraction on u *)
+
+let print_named_def name body typ =
+  let pbody = pr_lconstr body in
+  let ptyp = pr_ltype typ in
+  let pbody = if isCast body then surround pbody else pbody in
+  (str "*** [" ++ str name ++ str " " ++
+     hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
+	      str ":" ++ brk (1,2) ++ ptyp) ++
+	   str "]")
+
+let print_named_assum name typ =
+  str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
+
+let gallina_print_named_decl (id,c,typ) =
+  let s = string_of_id id in
+  match c with
+    | Some body -> print_named_def s body typ
+    | None -> print_named_assum s typ
+
+let assumptions_for_print lna =
+  List.fold_right (fun na env -> add_name na env) lna empty_names_context
+
+(*********************)
+(* *)
+
+let gallina_print_inductive sp =
+  let env = Global.env() in
+  let mib = Environ.lookup_mind sp env in
+  let mipv = mib.mind_packets in
+  pr_mutual_inductive_body env sp mib ++ fnl () ++
+  with_line_skip
+    (print_inductive_renames sp mipv @
+     print_inductive_implicit_args sp mipv @
+     print_inductive_argument_scopes sp mipv)
+
+let print_named_decl id =
+  gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
+
+let gallina_print_section_variable id =
+  print_named_decl id ++
+  with_line_skip (print_name_infos (VarRef id))
+
+let print_body = function
+  | Some lc  -> pr_lconstr (Declarations.force lc)
+  | None -> (str"<no body>")
+
+let print_typed_body (val_0,typ) =
+  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
+
+let ungeneralized_type_of_constant_type = function
+  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+  | NonPolymorphicType t -> t
+
+let print_constant with_values sep sp =
+  let cb = Global.lookup_constant sp in
+  let val_0 = body_of_constant cb in
+  let typ = ungeneralized_type_of_constant_type cb.const_type in
+  hov 0 (
+    match val_0 with
+    | None ->
+	str"*** [ " ++
+	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+	str" ]"
+    | _ ->
+	print_basename sp ++ str sep ++ cut () ++
+	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ))
+  ++ fnl ()
+
+let gallina_print_constant_with_infos sp =
+  print_constant true " = " sp ++
+  with_line_skip (print_name_infos (ConstRef sp))
+
+let gallina_print_syntactic_def kn =
+  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+  and (vars,a) = Syntax_def.search_syntactic_definition kn in
+  let c = Notation_ops.glob_constr_of_notation_constr dummy_loc a in
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
+        spc () ++ str ":=") ++
+     spc () ++ Constrextern.without_symbols pr_glob_constr c) ++ fnl ()
+
+let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
+  let sep = if with_values then " = " else " : "
+  and tag = object_tag lobj in
+    match (oname,tag) with
+      | (_,"VARIABLE") ->
+	  (* Outside sections, VARIABLES still exist but only with universes
+             constraints *)
+	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
+      | (_,"CONSTANT") ->
+	  Some (print_constant with_values sep (constant_of_kn kn))
+      | (_,"INDUCTIVE") ->
+	  Some (gallina_print_inductive (mind_of_kn kn))
+      | (_,"MODULE") ->
+	  let (mp,_,l) = repr_kn kn in
+	    Some (print_module with_values (MPdot (mp,l)))
+      | (_,"MODULE TYPE") ->
+	  let (mp,_,l) = repr_kn kn in
+	  Some (print_modtype (MPdot (mp,l)))
+      | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
+	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
+      (* To deal with forgotten cases... *)
+      | (_,s) -> None
+
+let gallina_print_library_entry with_values ent =
+  let pr_name (sp,_) = pr_id (basename sp) in
+  match ent with
+    | (oname,Lib.Leaf lobj) ->
+	gallina_print_leaf_entry with_values (oname,lobj)
+    | (oname,Lib.OpenedSection (dir,_)) ->
+        Some (str " >>>>>>> Section " ++ pr_name oname)
+    | (oname,Lib.ClosedSection _) ->
+        Some (str " >>>>>>> Closed Section " ++ pr_name oname)
+    | (_,Lib.CompilingLibrary (dir,_)) ->
+	Some (str " >>>>>>> Library " ++ pr_dirpath dir)
+    | (oname,Lib.OpenedModule _) ->
+	Some (str " >>>>>>> Module " ++ pr_name oname)
+    | (oname,Lib.ClosedModule _) ->
+        Some (str " >>>>>>> Closed Module " ++ pr_name oname)
+    | (_,Lib.FrozenState _) ->
+	None
+
+let gallina_print_context with_values =
+  let rec prec n = function
+    | h::rest when n = None or Option.get n > 0 ->
+	(match gallina_print_library_entry with_values h with
+	  | None -> prec n rest
+	  | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
+    | _ -> mt ()
+  in
+  prec
+
+let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} =
+  let ntrm = red_fun env evmap trm in
+  (str "     = " ++ gallina_print_typed_value_in_env env (ntrm,typ))
+
+(******************************************)
+(**** Printing abstraction layer          *)
+
+let default_object_pr = {
+  print_inductive           = gallina_print_inductive;
+  print_constant_with_infos = gallina_print_constant_with_infos;
+  print_section_variable    = gallina_print_section_variable;
+  print_syntactic_def       = gallina_print_syntactic_def;
+  print_module              = gallina_print_module;
+  print_modtype             = gallina_print_modtype;
+  print_named_decl          = gallina_print_named_decl;
+  print_library_entry       = gallina_print_library_entry;
+  print_context             = gallina_print_context;
+  print_typed_value_in_env  = gallina_print_typed_value_in_env;
+  print_eval                = gallina_print_eval;
+}
+
+let object_pr = ref default_object_pr
+let set_object_pr = (:=) object_pr
+
+let print_inductive x = !object_pr.print_inductive x
+let print_constant_with_infos c = !object_pr.print_constant_with_infos c
+let print_section_variable c = !object_pr.print_section_variable c
+let print_syntactic_def x = !object_pr.print_syntactic_def x
+let print_module x  = !object_pr.print_module  x
+let print_modtype x = !object_pr.print_modtype x
+let print_named_decl x = !object_pr.print_named_decl x
+let print_library_entry x = !object_pr.print_library_entry x
+let print_context x = !object_pr.print_context x
+let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
+let print_eval x = !object_pr.print_eval x
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Abstract layer                 *****)
+
+let print_typed_value x = print_typed_value_in_env (Global.env ()) x
+
+let print_judgment env {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env (trm, typ)
+
+let print_safe_judgment env j =
+  let trm = Safe_typing.j_val j in
+  let typ = Safe_typing.j_type j in
+  print_typed_value_in_env env (trm, typ)
+
+(*********************)
+(* *)
+
+let print_full_context () =
+  print_context true None (Lib.contents_after None)
+
+let print_full_context_typ () =
+  print_context false None (Lib.contents_after None)
+
+let print_full_pure_context () =
+  let rec prec = function
+  | ((_,kn),Lib.Leaf lobj)::rest ->
+      let pp = match object_tag lobj with
+      | "CONSTANT" ->
+	  let con = Global.constant_of_delta_kn kn in
+	  let cb = Global.lookup_constant con in
+	  let typ = ungeneralized_type_of_constant_type cb.const_type in
+	  hov 0 (
+	    match cb.const_body with
+	      | Undef _ ->
+		str "Parameter " ++
+		print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
+	      | OpaqueDef lc ->
+		str "Theorem " ++ print_basename con ++ cut () ++
+		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
+		str "Proof " ++ pr_lconstr (Declarations.force_opaque lc)
+	      | Def c ->
+		str "Definition " ++ print_basename con ++ cut () ++
+		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
+		pr_lconstr (Declarations.force c))
+          ++ str "." ++ fnl () ++ fnl ()
+      | "INDUCTIVE" ->
+	  let mind = Global.mind_of_delta_kn kn in
+	  let mib = Global.lookup_mind mind in
+	  pr_mutual_inductive_body (Global.env()) mind mib ++
+	    str "." ++ fnl () ++ fnl ()
+      | "MODULE" ->
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+      | "MODULE TYPE" ->
+	  (* TODO: make it reparsable *)
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+      | _ -> mt () in
+      prec rest ++ pp
+  | _::rest -> prec rest
+  | _ -> mt () in
+  prec (Lib.contents_after None)
+
+(* For printing an inductive definition with
+   its constructors and elimination,
+   assume that the declaration of constructors and eliminations
+   follows the definition of the inductive type *)
+
+(* This is designed to print the contents of an opened section *)
+let read_sec_context r =
+  let loc,qid = qualid_of_reference r in
+  let dir =
+    try Nametab.locate_section qid
+    with Not_found ->
+      user_err_loc (loc,"read_sec_context", str "Unknown section.") in
+  let rec get_cxt in_cxt = function
+    | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
+        if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | (_,Lib.ClosedSection _)::rest ->
+        error "Cannot print the contents of a closed section."
+	(* LEM: Actually, we could if we wanted to. *)
+    | [] -> []
+    | hd::rest -> get_cxt (hd::in_cxt) rest
+  in
+  let cxt = (Lib.contents_after None) in
+  List.rev (get_cxt [] cxt)
+
+let print_sec_context sec =
+  print_context true None (read_sec_context sec)
+
+let print_sec_context_typ sec =
+  print_context false None (read_sec_context sec)
+
+let print_any_name = function
+  | Term (ConstRef sp) -> print_constant_with_infos sp
+  | Term (IndRef (sp,_)) -> print_inductive sp
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
+  | Term (VarRef sp) -> print_section_variable sp
+  | Syntactic kn -> print_syntactic_def kn
+  | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
+  | Dir _ -> mt ()
+  | ModuleType (_,kn) -> print_modtype kn
+  | Undefined qid ->
+  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
+    let dir,str = repr_qualid qid in
+    if (repr_dirpath dir) <> [] then raise Not_found;
+    let (_,c,typ) = Global.lookup_named str in
+    (print_named_decl (str,c,typ))
+  with Not_found ->
+    errorlabstrm
+      "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+
+let print_name = function
+  | ByNotation (loc,ntn,sc) ->
+      print_any_name
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+               ntn sc))
+  | AN ref ->
+      print_any_name (locate_any_name ref)
+
+let print_opaque_name qid =
+  let env = Global.env () in
+  match global qid with
+    | ConstRef cst ->
+	let cb = Global.lookup_constant cst in
+        if constant_has_body cb then
+	  print_constant_with_infos cst
+        else
+	  error "Not a defined constant."
+    | IndRef (sp,_) ->
+        print_inductive sp
+    | ConstructRef cstr ->
+	let ty = Inductiveops.type_of_constructor env cstr in
+	print_typed_value (mkConstruct cstr, ty)
+    | VarRef id ->
+        let (_,c,ty) = lookup_named id env in
+	print_named_decl (id,c,ty)
+
+let print_about_any k =
+  match k with
+  | Term ref ->
+      pr_infos_list
+       ([print_ref false ref; blankline] @
+	print_name_infos ref @
+	print_simpl_behaviour ref @
+	print_opacity ref @
+	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+  | Syntactic kn ->
+      v 0 (
+      print_syntactic_def kn ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl()
+  | Dir _ | ModuleType _ | Undefined _ ->
+      hov 0 (pr_located_qualid k) ++ fnl()
+
+let print_about = function
+  | ByNotation (loc,ntn,sc) ->
+      print_about_any
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+               ntn sc))
+  | AN ref ->
+      print_about_any (locate_any_name ref)
+
+(* for debug *)
+let inspect depth =
+  print_context false (Some depth) (Lib.contents_after None)
+
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml                     *)
+
+open Classops
+
+let print_coercion_value v = pr_lconstr (get_coercion_value v)
+
+let print_class i =
+  let cl,_ = class_info_from_index i in
+  pr_class cl
+
+let print_path ((i,j),p) =
+  hov 2 (
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"] : ") ++
+  print_class i ++ str" >-> " ++ print_class j
+
+let _ = Classops.install_path_printer print_path
+
+let print_graph () =
+  prlist_with_sep fnl print_path (inheritance_graph())
+
+let print_classes () =
+  pr_sequence pr_class (classes())
+
+let print_coercions () =
+  pr_sequence print_coercion_value (coercions())
+
+let index_of_class cl =
+  try
+    fst (class_info cl)
+  with _ ->
+    errorlabstrm "index_of_class"
+      (pr_class cl ++ spc() ++ str "not a defined class.")
+
+let print_path_between cls clt =
+  let i = index_of_class cls in
+  let j = index_of_class clt in
+  let p =
+    try
+      lookup_path_between_class (i,j)
+    with _ ->
+      errorlabstrm "index_cl_of_id"
+        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
+	 ++ str ".")
+  in
+  print_path ((i,j),p)
+
+let print_canonical_projections () =
+  prlist_with_sep fnl
+    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+    str " <- " ++
+    pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+    (canonical_projections ())
+
+(*************************************************************************)
+
+(*************************************************************************)
+(* Pretty-printing functions for type classes                     *)
+
+open Typeclasses
+
+let pr_typeclass env t =
+  print_ref false t.cl_impl ++ fnl ()
+
+let print_typeclasses () =
+  let env = Global.env () in
+    prlist_with_sep fnl (pr_typeclass env) (typeclasses ())
+
+let pr_instance env i =
+  (*   gallina_print_constant_with_infos i.is_impl *)
+  (* lighter *)
+  print_ref false (instance_impl i) ++ fnl ()
+
+let print_all_instances () =
+  let env = Global.env () in
+  let inst = all_instances () in
+    prlist_with_sep fnl (pr_instance env) inst
+
+let print_instances r =
+  let env = Global.env () in
+  let inst = instances r in
+    prlist_with_sep fnl (pr_instance env) inst
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
new file mode 100644
index 000000000..dfd15a6d1
--- /dev/null
+++ b/printing/prettyp.mli
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Sign
+open Term
+open Environ
+open Reductionops
+open Libnames
+open Globnames
+open Nametab
+open Misctypes
+
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
+
+val assumptions_for_print : name list -> Termops.names_context
+
+val print_closed_sections : bool ref
+val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds
+val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option
+val print_full_context : unit -> std_ppcmds
+val print_full_context_typ : unit -> std_ppcmds
+val print_full_pure_context : unit -> std_ppcmds
+val print_sec_context : reference -> std_ppcmds
+val print_sec_context_typ : reference -> std_ppcmds
+val print_judgment : env -> unsafe_judgment -> std_ppcmds
+val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
+val print_eval :
+  reduction_function -> env -> Evd.evar_map ->
+    Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+
+val print_name : reference or_by_notation -> std_ppcmds
+val print_opaque_name : reference -> std_ppcmds
+val print_about : reference or_by_notation -> std_ppcmds
+val print_impargs : reference or_by_notation -> std_ppcmds
+
+(** Pretty-printing functions for classes and coercions *)
+val print_graph : unit -> std_ppcmds
+val print_classes : unit -> std_ppcmds
+val print_coercions : unit -> std_ppcmds
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
+val print_canonical_projections : unit -> std_ppcmds
+
+(** Pretty-printing functions for type classes and instances *)
+val print_typeclasses : unit -> std_ppcmds
+val print_instances : global_reference -> std_ppcmds
+val print_all_instances : unit -> std_ppcmds
+
+val inspect : int -> std_ppcmds
+
+(** Locate *)
+val print_located_qualid : reference -> std_ppcmds
+
+type object_pr = {
+  print_inductive           : mutual_inductive -> std_ppcmds;
+  print_constant_with_infos : constant -> std_ppcmds;
+  print_section_variable    : variable -> std_ppcmds;
+  print_syntactic_def       : kernel_name -> std_ppcmds;
+  print_module              : bool -> Names.module_path -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
+  print_named_decl          : identifier * constr option * types -> std_ppcmds;
+  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
+  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
+  print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
+  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+}
+
+val set_object_pr : object_pr -> unit
+val default_object_pr : object_pr
diff --git a/printing/printer.ml b/printing/printer.ml
new file mode 100644
index 000000000..1c51a6755
--- /dev/null
+++ b/printing/printer.ml
@@ -0,0 +1,700 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Sign
+open Environ
+open Global
+open Declare
+open Libnames
+open Globnames
+open Nametab
+open Evd
+open Proof_type
+open Refiner
+open Pfedit
+open Constrextern
+open Tacexpr
+open Ppconstr
+
+open Store.Field
+
+let emacs_str s =
+  if !Flags.print_emacs then s else ""
+let delayed_emacs_cmd s =
+  if !Flags.print_emacs then s () else str ""
+
+(**********************************************************************)
+(** Terms                                                             *)
+
+(* [goal_concl_style] means that all names of goal/section variables
+   and all names of rel variables (if any) in the given env and all short
+   names of global definitions of the current module must be avoided while
+   printing bound variables.
+   Otherwise, short names of global definitions are printed qualified
+   and only names of goal/section variables and rel names that do
+   _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+  pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+  pr_lconstr_expr (extern_constr goal_concl_style env t)
+
+let pr_lconstr_env env = pr_lconstr_core false env
+let pr_constr_env env = pr_constr_core false env
+
+let pr_open_lconstr_env env (_,c) = pr_lconstr_env env c
+let pr_open_constr_env env (_,c) = pr_constr_env env c
+
+  (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let pr_lconstr t = pr_lconstr_env (Global.env()) t
+let pr_constr t = pr_constr_env (Global.env()) t
+
+let pr_open_lconstr (_,c) = pr_lconstr c
+let pr_open_constr (_,c) = pr_constr c
+
+let pr_constr_under_binders_env_gen pr env (ids,c) =
+  (* Warning: clashes can occur with variables of same name in env but *)
+  (* we also need to preserve the actual names of the patterns *)
+  (* So what to do? *)
+  let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+  pr (Termops.push_rels_assum assums env) c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
+let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
+
+let pr_type_core goal_concl_style env t =
+  pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+  pr_lconstr_expr (extern_type goal_concl_style env t)
+
+let pr_goal_concl_style_env env = pr_ltype_core true env
+let pr_ltype_env env = pr_ltype_core false env
+let pr_type_env env = pr_type_core false env
+
+let pr_ltype t = pr_ltype_env (Global.env()) t
+let pr_type t = pr_type_env (Global.env()) t
+
+let pr_ljudge_env env j =
+  (pr_lconstr_env env j.uj_val, pr_lconstr_env env j.uj_type)
+
+let pr_ljudge j = pr_ljudge_env (Global.env()) j
+
+let pr_lglob_constr_env env c =
+  pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_glob_constr_env env c =
+  pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+
+let pr_lglob_constr c =
+  pr_lconstr_expr (extern_glob_constr Idset.empty c)
+let pr_glob_constr c =
+  pr_constr_expr (extern_glob_constr Idset.empty c)
+
+let pr_cases_pattern t =
+  pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
+
+let pr_lconstr_pattern_env env c =
+  pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
+let pr_constr_pattern_env env c =
+  pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
+
+let pr_lconstr_pattern t =
+  pr_lconstr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
+let pr_constr_pattern t =
+  pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
+
+let pr_sort s = pr_glob_sort (extern_sort s)
+
+let _ = Termops.set_print_constr pr_lconstr_env
+
+(**********************************************************************)
+(* Global references *)
+
+let pr_global_env = pr_global_env
+let pr_global = pr_global_env Idset.empty
+
+let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
+let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
+let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
+
+let pr_evaluable_reference ref =
+  pr_global (Tacred.global_of_evaluable_reference ref)
+
+(*let pr_glob_constr t =
+  pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*)
+
+(*open Pattern
+
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
+
+(**********************************************************************)
+(* Contexts and declarations                                          *)
+
+let pr_var_decl env (id,c,typ) =
+  let pbody = match c with
+    | None ->  (mt ())
+    | Some c ->
+	(* Force evaluation *)
+	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
+	(str" := " ++ pb ++ cut () ) in
+  let pt = pr_ltype_env env typ in
+  let ptyp = (str" : " ++ pt) in
+  (pr_id id ++ hov 0 (pbody ++ ptyp))
+
+let pr_rel_decl env (na,c,typ) =
+  let pbody = match c with
+    | None -> mt ()
+    | Some c ->
+	(* Force evaluation *)
+	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
+	(str":=" ++ spc () ++ pb ++ spc ()) in
+  let ptyp = pr_ltype_env env typ in
+  match na with
+  | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+  | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+
+
+(* Prints out an "env" in a nice format.  We print out the
+ * signature,then a horizontal bar, then the debruijn environment.
+ * It's printed out from outermost to innermost, so it's readable. *)
+
+(* Prints a signature, all declarations on the same line if possible *)
+let pr_named_context_of env =
+  let make_decl_list env d pps = pr_var_decl env d :: pps in
+  let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
+  hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
+
+let pr_named_context env ne_context =
+  hv 0 (Sign.fold_named_context
+	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+          ne_context ~init:(mt ()))
+
+let pr_rel_context env rel_context =
+  pr_binders (extern_rel_context None env rel_context)
+
+let pr_rel_context_of env =
+  pr_rel_context env (rel_context env)
+
+(* Prints an env (variables and de Bruijn). Separator: newline *)
+let pr_context_unlimited env =
+  let sign_env =
+    fold_named_context
+      (fun env d pps ->
+         let pidt =  pr_var_decl env d in (pps ++ fnl () ++ pidt))
+      env ~init:(mt ())
+  in
+  let db_env =
+    fold_rel_context
+      (fun env d pps ->
+         let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+      env ~init:(mt ())
+  in
+  (sign_env ++ db_env)
+
+let pr_ne_context_of header env =
+  if Environ.rel_context env = empty_rel_context &
+    Environ.named_context env = empty_named_context  then (mt ())
+  else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ())
+
+let pr_context_limit n env =
+  let named_context = Environ.named_context env in
+  let lgsign = List.length named_context in
+  if n >= lgsign then
+    pr_context_unlimited env
+  else
+    let k = lgsign-n in
+    let _,sign_env =
+      fold_named_context
+        (fun env d (i,pps) ->
+           if i < k then
+	     (i+1, (pps ++str "."))
+	   else
+             let pidt = pr_var_decl env d in
+	     (i+1, (pps ++ fnl () ++
+		      str (emacs_str "") ++
+		      pidt)))
+        env ~init:(0,(mt ()))
+    in
+    let db_env =
+      fold_rel_context
+        (fun env d pps ->
+           let pnat = pr_rel_decl env d in
+	   (pps ++ fnl () ++
+	      str (emacs_str "") ++
+	      pnat))
+        env ~init:(mt ())
+    in
+    (sign_env ++ db_env)
+
+let pr_context_of env = match Flags.print_hyps_limit () with
+  | None -> hv 0 (pr_context_unlimited env)
+  | Some n -> hv 0 (pr_context_limit n env)
+
+(* display goal parts (Proof mode) *)
+
+let pr_predicate pr_elt (b, elts) =
+  let pr_elts = prlist_with_sep spc pr_elt elts in
+    if b then
+      str"all" ++
+	(if elts = [] then mt () else str" except: " ++ pr_elts)
+    else
+      if elts = [] then str"none" else pr_elts
+
+let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
+let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
+
+let pr_transparent_state (ids, csts) =
+  hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
+	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+
+(* display complete goal *)
+let default_pr_goal gs =
+  let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
+  let env = Goal.V82.unfiltered_env sigma g in
+  let preamb,thesis,penv,pc =
+    mt (), mt (),
+    pr_context_of env,
+    pr_goal_concl_style_env env (Goal.V82.concl sigma g)
+  in
+    preamb ++
+    str"  " ++ hv 0 (penv ++ fnl () ++
+		       str (emacs_str "")  ++
+		       str "============================" ++ fnl ()  ++
+		       thesis ++ str " " ++  pc) ++ fnl ()
+
+(* display a goal tag *)
+let pr_goal_tag g =
+  let s = " (ID " ^ Goal.uid g ^ ")" in
+  str (emacs_str s)
+
+(* display the conclusion of a goal *)
+let pr_concl n sigma g =
+  let (g,sigma) = Goal.V82.nf_evar sigma g in
+  let env = Goal.V82.env sigma g in
+  let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
+    str (emacs_str "")  ++
+      str "subgoal " ++ int n ++ pr_goal_tag g ++
+      str " is:" ++ cut () ++ str" "  ++ pc
+
+(* display evar type: a context and a type *)
+let pr_evgl_sign gl =
+  let ps = pr_named_context_of (evar_unfiltered_env gl) in
+  let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
+  let ids = List.rev (List.map pi1 l) in
+  let warn =
+    if ids = [] then mt () else
+      (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
+  in
+  let pc = pr_lconstr gl.evar_concl in
+  hov 0 (str"[" ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]" ++ spc () ++ warn)
+
+(* Print an existential variable *)
+
+let pr_evar (ev, evd) =
+  let pegl = pr_evgl_sign evd in
+  (hov 0 (str (string_of_existential ev)  ++ str " : " ++ pegl))
+
+(* Print an enumerated list of existential variables *)
+let rec pr_evars_int i = function
+  | [] -> (mt ())
+  | (ev,evd)::rest ->
+      let pegl = pr_evgl_sign evd in
+      let pei = pr_evars_int (i+1) rest in
+      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++
+      fnl () ++ pei
+
+let default_pr_subgoal n sigma =
+  let rec prrec p = function
+    | [] -> error "No such goal."
+    | g::rest ->
+	if p = 1 then
+          let pg = default_pr_goal { sigma=sigma ; it=g } in
+          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
+	       ++ str " is:" ++ cut () ++ pg)
+	else
+	  prrec (p-1) rest
+  in
+  prrec n
+
+let emacs_print_dependent_evars sigma seeds =
+  let evars () =
+    let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in
+    let evars =
+      Intmap.fold begin fun e i s ->
+	let e' = str (string_of_existential e) in
+	match i with
+	| None -> s ++ str" " ++ e' ++ str " open,"
+	| Some i ->
+	  s ++ str " " ++ e' ++ str " using " ++
+	    Intset.fold begin fun d s ->
+	      str (string_of_existential d) ++ str " " ++ s
+	    end i (str ",")
+      end evars (str "")
+    in
+    cut () ++
+    str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+  in
+  delayed_emacs_cmd evars
+
+(* Print open subgoals. Checks for uninstantiated existential variables *)
+(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
+let default_pr_subgoals close_cmd sigma seeds = function
+  | [] ->
+      begin
+	match close_cmd with
+	  Some cmd ->
+	    (str "Subproof completed, now type " ++ str cmd ++
+	       str "." ++ fnl ())
+	| None ->
+	    let exl = Evarutil.non_instantiated sigma in
+	      if exl = [] then
+		(str"No more subgoals." ++ fnl ()
+		 ++ emacs_print_dependent_evars sigma seeds)
+	      else
+		let pei = pr_evars_int 1 exl in
+		  (str "No more subgoals but non-instantiated existential " ++
+		     str "variables:" ++ fnl () ++ (hov 0 pei)
+		   ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+                   str "You can use Grab Existential Variables.")
+      end
+  | [g] ->
+      let pg = default_pr_goal { it = g ; sigma = sigma } in
+      v 0 (
+	str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg
+	++ emacs_print_dependent_evars sigma seeds
+      )
+  | g1::rest ->
+      let rec pr_rec n = function
+        | [] -> (mt ())
+        | g::rest ->
+            let pc = pr_concl n sigma g in
+            let prest = pr_rec (n+1) rest in
+            (cut () ++ pc ++ prest)
+      in
+      let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
+      let prest = pr_rec 2 rest in
+      v 0 (
+	int(List.length rest+1) ++ str" subgoals" ++
+          str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
+	++ pg1 ++ prest ++ fnl ()
+	++ emacs_print_dependent_evars sigma seeds
+      )
+
+(**********************************************************************)
+(* Abstraction layer                                                  *)
+
+
+type printer_pr = {
+ pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
+ pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal                : goal sigma -> std_ppcmds;
+}
+
+let default_printer_pr = {
+ pr_subgoals = default_pr_subgoals;
+ pr_subgoal  = default_pr_subgoal;
+ pr_goal     = default_pr_goal;
+}
+
+let printer_pr = ref default_printer_pr
+
+let set_printer_pr = (:=) printer_pr
+
+let pr_subgoals x = !printer_pr.pr_subgoals x
+let pr_subgoal  x = !printer_pr.pr_subgoal  x
+let pr_goal     x = !printer_pr.pr_goal     x
+
+(* End abstraction layer                                              *)
+(**********************************************************************)
+
+let pr_open_subgoals () =
+  let p = Proof_global.give_me_the_proof () in
+  let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
+  let seeds = Proof.V82.top_evars p in
+  begin match goals with
+  | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+            begin match bgoals with
+	    | [] -> pr_subgoals None sigma seeds goals
+	    | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
+		      str"This subproof is complete, but there are still unfocused goals." ++ fnl ()
+		(* spiwack: to stay compatible with the proof general and coqide,
+		    I use print the message after the goal. It would be better to have
+		    something like:
+		      str"This subproof is complete, but there are still unfocused goals:"
+		      ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
+		    instead. But it doesn't quite work.
+		*)
+	    end
+  | _ -> pr_subgoals None sigma seeds goals
+  end
+
+let pr_nth_open_subgoal n =
+  let pf = get_pftreestate () in
+  let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+  pr_subgoal n sigma gls
+
+let pr_goal_by_id id =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid id in
+  let pr gs =
+    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+	 ++ pr_goal gs)
+  in
+  try
+    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma})
+  with Not_found -> error "Invalid goal identifier."
+
+(* Elementary tactics *)
+
+let pr_prim_rule = function
+  | Intro id ->
+      str"intro " ++ pr_id id
+
+  | Cut (b,replace,id,t) ->
+     if b then
+       (* TODO: express "replace" *)
+       (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
+     else
+       let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
+       (str"cut " ++ pr_constr t ++
+        str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
+
+  | FixRule (f,n,[],_) ->
+      (str"fix " ++ pr_id f ++ str"/" ++ int n)
+
+  | FixRule (f,n,others,j) ->
+      if j<>0 then warning "Unsupported printing of \"fix\"";
+      let rec print_mut = function
+	| (f,n,ar)::oth ->
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
+        | [] -> mt () in
+      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[],_) ->
+      (str"cofix " ++ pr_id f)
+
+  | Cofix (f,others,j) ->
+      if j<>0 then warning "Unsupported printing of \"fix\"";
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+  | Refine c ->
+      str(if Termops.occur_meta c then "refine " else "exact ") ++
+      Constrextern.with_meta_as_hole pr_constr c
+
+  | Convert_concl (c,_) ->
+      (str"change "  ++ pr_constr c)
+
+  | Convert_hyp (id,None,t) ->
+      (str"change "  ++ pr_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"change "  ++ pr_constr c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
+
+  | Thin ids ->
+      (str"clear "  ++ pr_sequence pr_id ids)
+
+  | ThinBody ids ->
+      (str"clearbody "  ++ pr_sequence pr_id ids)
+
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "dependent " else "") ++
+	 str"move "  ++ pr_id id1 ++ Miscops.pr_move_location pr_id id2)
+
+  | Order ord ->
+      (str"order "  ++ pr_sequence pr_id ord)
+
+  | Rename (id1,id2) ->
+      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+  | Change_evars ->
+      (* This is internal tactic and cannot be replayed at user-level.
+         Function pr_rule_dot below is used when we want to hide
+         Change_evars *)
+      str "Evar change"
+
+
+(* Backwards compatibility *)
+
+let prterm = pr_lconstr
+
+
+(* Printer function for sets of Assumptions.assumptions.
+   It is used primarily by the Print Assumptions command. *)
+
+open Assumptions
+
+let pr_assumptionset env s =
+  if ContextObjectMap.is_empty s then
+    str "Closed under the global context" ++ fnl()
+  else
+    let safe_pr_constant env kn =
+      try pr_constant env kn
+      with Not_found ->
+	let mp,_,lab = repr_con kn in
+	str (string_of_mp mp ^ "." ^ string_of_label lab)
+    in
+    let safe_pr_ltype typ =
+      try str " : " ++ pr_ltype typ with _ -> mt ()
+    in
+    let (vars,axioms,opaque) =
+      ContextObjectMap.fold (fun t typ r ->
+	let (v,a,o) = r in
+	match t with
+	| Variable id -> (  Some (
+	                      Option.default (fnl ()) v
+			   ++ str (string_of_id id)
+			   ++ str " : "
+	                   ++ pr_ltype typ
+	                   ++ fnl ()
+			    )
+	                 ,
+	                   a, o)
+	| Axiom kn    -> ( v ,
+			     Some (
+			      Option.default (fnl ()) a
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 , o
+			 )
+	| Opaque kn    -> ( v , a ,
+			     Some (
+			      Option.default (fnl ()) o
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 )
+      )
+	s (None,None,None)
+    in
+    let (vars,axioms,opaque) =
+      ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
+	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
+      )
+    in
+    (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+      ++ (Option.default (mt ()) opaque)
+
+let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
+
+open Typeclasses
+
+let pr_instance i =
+  pr_global (instance_impl i)
+
+let pr_instance_gmap insts =
+  prlist_with_sep fnl (fun (gr, insts) ->
+    prlist_with_sep fnl pr_instance (cmap_to_list insts))
+    (Gmap.to_list insts)
+
+(** Inductive declarations *)
+
+open Declarations
+open Termops
+open Reduction
+open Inductive
+open Inductiveops
+
+let print_params env params =
+  if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
+
+let print_constructors envpar names types =
+  let pc =
+    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+      (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
+      (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
+  in
+  hv 0 (str "  " ++ pc)
+
+let build_ind_type env mip =
+  match mip.mind_arity with
+    | Monomorphic ar -> ar.mind_user_arity
+    | Polymorphic ar ->
+      it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
+
+let print_one_inductive env mib ((_,i) as ind) =
+  let mip = mib.mind_packets.(i) in
+  let params = mib.mind_params_ctxt in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env (build_ind_type env mip) args in
+  let cstrtypes = Inductive.type_of_constructors ind (mib,mip) in
+  let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+  let envpar = push_rel_context params env in
+  hov 0 (
+    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++
+    str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib =
+  let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
+  in
+  hov 0 (
+    str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
+    prlist_with_sep (fun () -> fnl () ++ str"  with ")
+      (print_one_inductive env mib) inds)
+
+let get_fields =
+  let rec prodec_rec l subst c =
+    match kind_of_term c with
+    | Prod (na,t,c) ->
+	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
+    | LetIn (na,b,_,c) ->
+	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
+    | _               -> List.rev l
+  in
+  prodec_rec [] []
+
+let print_record env mind mib =
+  let mip = mib.mind_packets.(0) in
+  let params = mib.mind_params_ctxt in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env (build_ind_type env mip) args in
+  let cstrtypes = Inductive.type_of_constructors (mind,0) (mib,mip) in
+  let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+  let fields = get_fields cstrtype in
+  let envpar = push_rel_context params env in
+  hov 0 (
+    hov 0 (
+      str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++
+      print_params env params ++
+      str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
+      str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+    brk(1,2) ++
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+        (fun (id,b,c) ->
+	  pr_id id ++ str (if b then " : " else " := ") ++
+	  pr_lconstr_env envpar c) fields) ++ str" }")
+
+let pr_mutual_inductive_body env mind mib =
+  if mib.mind_record & not !Flags.raw_print then
+    print_record env mind mib
+  else
+    print_mutual_inductive env mind mib
diff --git a/printing/printer.mli b/printing/printer.mli
new file mode 100644
index 000000000..3b9ef8ecc
--- /dev/null
+++ b/printing/printer.mli
@@ -0,0 +1,159 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Libnames
+open Globnames
+open Term
+open Sign
+open Environ
+open Glob_term
+open Pattern
+open Nametab
+open Termops
+open Evd
+open Proof_type
+open Glob_term
+open Tacexpr
+
+(** These are the entry points for printing terms, context, tac, ... *)
+
+(** Terms *)
+
+val pr_lconstr_env         : env -> constr -> std_ppcmds
+val pr_lconstr             : constr -> std_ppcmds
+
+val pr_constr_env          : env -> constr -> std_ppcmds
+val pr_constr              : constr -> std_ppcmds
+
+val pr_open_constr_env     : env -> open_constr -> std_ppcmds
+val pr_open_constr         : open_constr -> std_ppcmds
+
+val pr_open_lconstr_env    : env -> open_constr -> std_ppcmds
+val pr_open_lconstr        : open_constr -> std_ppcmds
+
+val pr_constr_under_binders_env  : env -> constr_under_binders -> std_ppcmds
+val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+
+val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
+val pr_ltype_env           : env -> types -> std_ppcmds
+val pr_ltype               : types -> std_ppcmds
+
+val pr_type_env            : env -> types -> std_ppcmds
+val pr_type                : types -> std_ppcmds
+
+val pr_ljudge_env          : env -> unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
+
+val pr_lglob_constr_env      : env -> glob_constr -> std_ppcmds
+val pr_lglob_constr          : glob_constr -> std_ppcmds
+
+val pr_glob_constr_env       : env -> glob_constr -> std_ppcmds
+val pr_glob_constr           : glob_constr -> std_ppcmds
+
+val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds
+val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
+
+val pr_constr_pattern_env  : env -> constr_pattern -> std_ppcmds
+val pr_constr_pattern      : constr_pattern -> std_ppcmds
+
+val pr_cases_pattern       : cases_pattern -> std_ppcmds
+
+val pr_sort                : sorts -> std_ppcmds
+
+(** Printing global references using names as short as possible *)
+
+val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
+val pr_global              : global_reference -> std_ppcmds
+
+val pr_constant            : env -> constant -> std_ppcmds
+val pr_existential         : env -> existential -> std_ppcmds
+val pr_constructor         : env -> constructor -> std_ppcmds
+val pr_inductive           : env -> inductive -> std_ppcmds
+val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+
+(** Contexts *)
+
+val pr_ne_context_of       : std_ppcmds -> env -> std_ppcmds
+
+val pr_var_decl            : env -> named_declaration -> std_ppcmds
+val pr_rel_decl            : env -> rel_declaration -> std_ppcmds
+
+val pr_named_context       : env -> named_context -> std_ppcmds
+val pr_named_context_of    : env -> std_ppcmds
+val pr_rel_context         : env -> rel_context -> std_ppcmds
+val pr_rel_context_of      : env -> std_ppcmds
+val pr_context_of          : env -> std_ppcmds
+
+(** Predicates *)
+
+val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
+val pr_cpred               : Cpred.t -> std_ppcmds
+val pr_idpred              : Idpred.t -> std_ppcmds
+val pr_transparent_state   : transparent_state -> std_ppcmds
+
+(** Proofs *)
+
+val pr_goal                : goal sigma -> std_ppcmds
+val pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds
+val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
+val pr_concl               : int -> evar_map -> goal -> std_ppcmds
+
+val pr_open_subgoals       : unit -> std_ppcmds
+val pr_nth_open_subgoal    : int -> std_ppcmds
+val pr_evar                : (evar * evar_info) -> std_ppcmds
+val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
+
+val pr_prim_rule           : prim_rule -> std_ppcmds
+
+(** Emacs/proof general support
+   (emacs_str s) outputs
+    - s if emacs mode,
+    - nothing otherwise.
+    This function was previously used to insert special chars like
+    [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the
+    proof context for proof by pointing. This part of the code is
+    removed for now because it interacted badly with utf8. We may put
+    it back some day using some xml-like tags instead of special
+    chars. See for example the <prompt> tag in the prompt when in
+    emacs mode. *)
+val emacs_str              : string -> string
+
+(** Backwards compatibility *)
+
+val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
+
+
+(** spiwack: printer function for sets of Environ.assumption.
+            It is used primarily by the Print Assumption command. *)
+val pr_assumptionset :
+  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+
+val pr_goal_by_id : string -> std_ppcmds
+
+type printer_pr = {
+ pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
+ pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal                : goal sigma -> std_ppcmds;
+};;
+
+val set_printer_pr : printer_pr -> unit
+
+val default_printer_pr : printer_pr
+
+val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
+  Pp.std_ppcmds
+
+(** Inductive declarations *)
+
+val pr_mutual_inductive_body :
+  env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
diff --git a/printing/printing.mllib b/printing/printing.mllib
new file mode 100644
index 000000000..f7fbe4e13
--- /dev/null
+++ b/printing/printing.mllib
@@ -0,0 +1,6 @@
+Ppconstr
+Printer
+Pptactic
+Tactic_printer
+Printmod
+Prettyp
\ No newline at end of file
diff --git a/printing/printmod.ml b/printing/printmod.ml
new file mode 100644
index 000000000..1953935aa
--- /dev/null
+++ b/printing/printmod.ml
@@ -0,0 +1,259 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Names
+open Declarations
+open Nameops
+open Globnames
+open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+    - The "short" one, that just prints the names of the fields.
+    - The "rich" one, that also tries to print the types of the fields.
+    The short version used to be the default behavior, but now we print
+    types by default. The following option allows to change this.
+    Technically, the environments in this file are either None in
+    the "short" mode or (Some env) in the "rich" one.
+*)
+
+let short = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "short module printing";
+      optkey   = ["Short";"Module";"Printing"];
+      optread  = (fun () -> !short) ;
+      optwrite = ((:=) short) }
+
+let get_new_id locals id =
+  let rec get_id l id =
+    let dir = make_dirpath [id] in
+      if not (Nametab.exists_module dir) then
+	id
+      else
+	get_id (id::l) (Namegen.next_ident_away id l)
+  in
+    get_id (List.map snd locals) id
+
+let rec print_local_modpath locals = function
+  | MPbound mbid -> pr_id (List.assoc mbid locals)
+  | MPdot(mp,l) ->
+      print_local_modpath locals mp ++ str "." ++ pr_lab l
+  | MPfile _ -> raise Not_found
+
+let print_modpath locals mp =
+  try (* must be with let because streams are lazy! *)
+    let qid = Nametab.shortest_qualid_of_module mp in
+      pr_qualid qid
+  with
+    | Not_found -> print_local_modpath locals mp
+
+let print_kn locals kn =
+  try
+    let qid = Nametab.shortest_qualid_of_modtype kn in
+      pr_qualid qid
+  with
+      Not_found ->
+	try
+	  print_local_modpath locals kn
+	with
+	    Not_found -> print_modpath locals kn
+
+let nametab_register_dir mp =
+  let id = id_of_string "FAKETOP" in
+  let fp = Libnames.make_path empty_dirpath id in
+  let dir = make_dirpath [id] in
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
+  fp
+
+(** Nota: the [global_reference] we register in the nametab below
+    might differ from internal ones, since we cannot recreate here
+    the canonical part of constant and inductive names, but only
+    the user names. This works nonetheless since we search now
+    [Nametab.the_globrevtab] modulo user name. *)
+
+let nametab_register_body mp fp (l,body) =
+  let push id ref =
+    Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
+  in
+  match body with
+    | SFBmodule _ -> () (* TODO *)
+    | SFBmodtype _ -> () (* TODO *)
+    | SFBconst _ ->
+      push (id_of_label l) (ConstRef (make_con mp empty_dirpath l))
+    | SFBmind mib ->
+      let mind = make_mind mp empty_dirpath l in
+      Array.iteri
+	(fun i mip ->
+	  push mip.mind_typename (IndRef (mind,i));
+	  Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1)))
+	    mip.mind_consnames)
+	mib.mind_packets
+
+let print_body is_impl env mp (l,body) =
+  let name = str (string_of_label l) in
+  hov 2 (match body with
+    | SFBmodule _ -> str "Module " ++ name
+    | SFBmodtype _ -> str "Module Type " ++ name
+    | SFBconst cb ->
+      (match cb.const_body with
+	| Def _ -> str "Definition "
+	| OpaqueDef _ when is_impl -> str "Theorem "
+	| _ -> str "Parameter ") ++ name ++
+      (match env with
+	  | None -> mt ()
+	  | Some env ->
+	    str " :" ++ spc () ++
+	    hov 0 (Printer.pr_ltype_env env
+		     (Typeops.type_of_constant_type env cb.const_type)) ++
+	    (match cb.const_body with
+	      | Def l when is_impl ->
+		spc () ++
+		hov 2 (str ":= " ++
+		       Printer.pr_lconstr_env env (Declarations.force l))
+	      | _ -> mt ()) ++
+            str ".")
+    | SFBmind mib ->
+      try
+	let env = Option.get env in
+	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
+      with _ ->
+	(if mib.mind_finite then str "Inductive " else str "CoInductive")
+	++ name)
+
+let print_struct is_impl env mp struc =
+  begin
+    (* If [mp] is a globally visible module, we simply import it *)
+    try Declaremods.really_import_module mp
+    with _ ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+      let fp = nametab_register_dir mp in
+      List.iter (nametab_register_body mp fp) struc
+  end;
+  prlist_with_sep spc (print_body is_impl env mp) struc
+
+let rec flatten_app mexpr l = match mexpr with
+  | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l)
+  | SEBident mp -> mp::l
+  | _ -> assert false
+
+let rec print_modtype env mp locals mty =
+  match mty with
+    | SEBident kn -> print_kn locals kn
+    | SEBfunctor (mbid,mtb1,mtb2) ->
+      let mp1 = MPbound mbid in
+      let env' = Option.map
+	  (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
+      let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
+      in
+      (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+      hov 2 (str "Funsig" ++ spc () ++ str "(" ++
+	       pr_id (id_of_mbid mbid) ++ str ":" ++
+	       print_modtype env mp1 locals seb1 ++
+	       str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
+  | SEBstruct (sign) ->
+      let env' = Option.map
+	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+      hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
+	    brk (1,-2) ++ str "End")
+  | SEBapply _ ->
+      let lapp = flatten_app mty [] in
+      let fapp = List.hd lapp in
+      let mapp = List.tl lapp in
+      hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
+		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
+  | SEBwith(seb,With_definition_body(idl,cb))->
+      let env' = None in (* TODO: build a proper environment if env <> None *)
+      let s = (String.concat "." (List.map string_of_id idl)) in
+      hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
+	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
+  | SEBwith(seb,With_module_body(idl,mp))->
+      let s =(String.concat "." (List.map string_of_id idl)) in
+      hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
+	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+
+let rec print_modexpr env mp locals mexpr = match mexpr with
+  | SEBident mp -> print_modpath locals mp
+  | SEBfunctor (mbid,mty,mexpr) ->
+      let mp' = MPbound mbid in
+      let env' = Option.map
+	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
+      let typ = Option.default mty.typ_expr mty.typ_expr_alg in
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
+      (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
+      hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
+	     str ":" ++ print_modtype env mp' locals typ ++
+      str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
+  | SEBstruct struc ->
+      let env' = Option.map
+	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+      hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
+	    brk (1,-2) ++ str "End")
+  | SEBapply _ ->
+      let lapp = flatten_app mexpr [] in
+      hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | SEBwith (_,_)-> anomaly "Not available yet"
+
+
+let rec printable_body dir =
+  let dir = pop_dirpath dir in
+    dir = empty_dirpath ||
+    try
+      match Nametab.locate_dir (qualid_of_dirpath dir) with
+	  DirOpenModtype _ -> false
+	| DirModule _ | DirOpenModule _ -> printable_body dir
+	| _ -> true
+    with
+	Not_found -> true
+
+(** Since we might play with nametab above, we should reset to prior
+    state after the printing *)
+
+let print_modexpr' env mp mexpr =
+  States.with_state_protection (print_modexpr env mp []) mexpr
+let print_modtype' env mp mty =
+  States.with_state_protection (print_modtype env mp []) mty
+
+let print_module' env mp with_body mb =
+  let name = print_modpath [] mp in
+  let body = match with_body, mb.mod_expr with
+    | false, _
+    | true, None -> mt()
+    | true, Some mexpr ->
+	spc () ++ str ":= " ++ print_modexpr' env mp mexpr
+  in
+  let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type
+  in
+  hv 0 (str "Module " ++ name ++ modtype ++ body)
+
+exception ShortPrinting
+
+let print_module with_body mp =
+  let me = Global.lookup_module mp in
+  try
+    if !short then raise ShortPrinting;
+    print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
+  with _ ->
+    print_module' None mp with_body me ++ fnl ()
+
+let print_modtype kn =
+  let mtb = Global.lookup_modtype kn in
+  let name = print_kn [] kn in
+  hv 1
+    (str "Module Type " ++ name ++ str " =" ++ spc () ++
+     (try
+	if !short then raise ShortPrinting;
+	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+      with _ ->
+	print_modtype' None kn mtb.typ_expr))
diff --git a/printing/printmod.mli b/printing/printmod.mli
new file mode 100644
index 000000000..348d88bf5
--- /dev/null
+++ b/printing/printmod.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** false iff the module is an element of an open module type *)
+val printable_body : dir_path -> bool
+
+val print_module : bool -> module_path -> Pp.std_ppcmds
+
+val print_modtype : module_path -> Pp.std_ppcmds
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
new file mode 100644
index 000000000..2c51abcd0
--- /dev/null
+++ b/printing/tactic_printer.ml
@@ -0,0 +1,170 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Sign
+open Evd
+open Tacexpr
+open Proof_type
+open Printer
+
+let pr_tactic = function
+  | TacArg (_,Tacexp t) ->
+      (*top tactic from tacinterp*)
+      Pptactic.pr_glob_tactic (Global.env()) t
+  | t ->
+      Pptactic.pr_tactic (Global.env()) t
+
+let pr_rule = function
+  | Prim r -> hov 0 (pr_prim_rule r)
+  | Nested(cmpd,_) ->
+      begin
+	match cmpd with
+	  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+      end
+  | Daimon -> str "<Daimon>"
+  | Decl_proof _ -> str "proof"
+
+let uses_default_tac = function
+  | Nested(Tactic(_,dflt),_) -> dflt
+  | _ -> false
+
+(* Does not print change of evars *)
+let pr_rule_dot = function
+  | Prim Change_evars ->str "PC: ch_evars" ++  mt ()
+      (* PC: this might be redundant *)
+  | r ->
+      pr_rule r ++ if uses_default_tac r then str "..." else str"."
+
+let pr_rule_dot_fnl = function
+  | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
+                              | TacMutualCofix (true,_,_))),_),_) ->
+      (* Very big hack to not display hidden tactics in "Theorem with" *)
+      (* (would not scale!) *)
+      mt ()
+   | Prim Change_evars -> mt ()
+   | r -> pr_rule_dot r ++ fnl ()
+
+exception Different
+
+let rec print_proof sigma osign pf =
+  (* spiwack: [osign] is currently ignored, not sure if this function is even used. *)
+  let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in
+  match pf.ref with
+    | None ->
+	hov 0 (pr_goal {sigma = sigma; it=pf.goal })
+    | Some(r,spfl) ->
+	hov 0
+	  (hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++
+	   spc () ++ str" BY " ++
+	   hov 0 (pr_rule r) ++ fnl () ++
+	   str"  " ++
+	   hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl))
+
+let pr_change sigma gl =
+  str"change " ++
+  pr_lconstr_env (Goal.V82.env sigma gl) (Goal.V82.concl sigma gl) ++ str"."
+
+let print_decl_script tac_printer ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+  match pf.ref with
+    | None ->
+	(if nochange then
+	   (str"<Your Proof Text here>")
+	 else
+	   pr_change sigma pf.goal)
+	++ fnl ()
+    | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
+    | Some (Prim Change_evars,[subpf]) -> print_prf subpf
+    | _ -> anomaly "Not Applicable" in
+  print_prf pf
+
+let print_script ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+  match pf.ref with
+    | None ->
+        (if nochange then
+	   (str"<Your Tactic Text here>")
+	 else
+	   pr_change sigma pf.goal)
+	++ fnl ()
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())
+	end ++
+	  begin
+	    hov 0 (str "proof." ++ fnl () ++
+		     print_decl_script print_prf
+		     ~nochange sigma (List.hd script))
+	  end ++ fnl () ++
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
+	   prlist_with_sep fnl print_prf spfl )
+    | Some(rule,spfl) ->
+	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
+	   pr_rule_dot_fnl rule ++
+	   prlist_with_sep fnl print_prf spfl ) in
+  print_prf pf
+
+(* printed by Show Script command *)
+
+let print_treescript ?(nochange=true) sigma pf =
+  let rec print_prf pf =
+    match pf.ref with
+    | None ->
+        if nochange then
+	  str"<Your Proof Text here>"
+	else pr_change sigma pf.goal
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then mt () else pr_change sigma pf.goal ++ fnl ()
+	end ++
+	hov 0
+	  begin str "proof." ++ fnl () ++
+	    print_decl_script print_prf ~nochange sigma (List.hd script)
+	  end ++ fnl () ++
+	begin
+	  if opened then mt () else (str "end proof." ++ fnl ())
+	end
+    | Some(Daimon,spfl) ->
+	(if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
+	prlist_with_sep fnl (print_script ~nochange sigma) spfl
+    | Some(r,spfl) ->
+        let indent = if List.length spfl >= 2 then 1 else 0 in
+        (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
+        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
+  in hov 0 (print_prf pf)
+
+let rec print_info_script sigma osign pf =
+  let sign = Goal.V82.hyps sigma pf.goal in
+  match pf.ref with
+    | None -> (mt ())
+    | Some(r,spfl) ->
+        (pr_rule r ++
+           match spfl with
+             | [pf1] ->
+                 if pf1.ref = None then
+		   (str "." ++ fnl ())
+                 else
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma
+		      (Environ.named_context_of_val sign) pf1)
+             | _ -> (str"." ++ fnl () ++
+                       prlist_with_sep fnl
+                         (print_info_script sigma
+			    (Environ.named_context_of_val sign)) spfl))
+
+let format_print_info_script sigma osign pf =
+  hov 0 (print_info_script sigma osign pf)
diff --git a/printing/tactic_printer.mli b/printing/tactic_printer.mli
new file mode 100644
index 000000000..5ea579107
--- /dev/null
+++ b/printing/tactic_printer.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Sign
+open Evd
+open Tacexpr
+open Proof_type
+
+(** These are the entry points for tactics, proof trees, ... *)
+
+val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
+val pr_rule     : rule -> std_ppcmds
+val pr_tactic   : tactic_expr -> std_ppcmds
+val print_script :
+  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
+val print_treescript :
+  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds