Ajout du traducteur

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

6 files changed, 1569 insertions, 0 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
new file mode 100644
index 0000000000..7d6899f77b
--- /dev/null
+++ b/translate/ppconstrnew.ml
@@ -0,0 +1,370 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)      
+
+open Ast
+open Util
+open Pp
+open Nametab
+open Names
+open Nameops
+open Libnames
+open Coqast
+open Ppextend
+open Topconstr
+open Term
+
+let sep = fun _ -> spc()
+let sep_p = fun _ -> str"."
+let sep_v = fun _ -> str","
+let sep_pp = fun _ -> str":"
+let sep_pv = fun _ -> str"; "
+
+let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
+
+let pr_global ref = pr_global_env None ref
+
+let global_const_name kn =
+  try pr_global (ConstRef kn)
+  with Not_found -> (str ("CONST("^(string_of_kn kn)^")"))
+
+let global_var_name id =
+  try pr_global (VarRef id)
+  with Not_found -> (str ("SECVAR("^(string_of_id id)^")"))
+
+let global_ind_name (kn,tyi) =
+  try pr_global (IndRef (kn,tyi))
+  with Not_found -> (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
+
+let global_constr_name ((kn,tyi),i) =
+  try pr_global (ConstructRef ((kn,tyi),i))
+  with Not_found -> (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)^","^(string_of_int i)^")"))
+
+let globpr gt = match gt with
+  | Nvar(_,s) -> (pr_id s)
+  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
+  | Node(_,"CONST",[Path(_,sl)]) ->
+      global_const_name (section_path sl)
+  | Node(_,"SECVAR",[Nvar(_,s)]) ->
+      global_var_name s
+  | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
+      global_ind_name (section_path sl, tyi)
+  | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
+      global_constr_name ((section_path sl, tyi), i)
+  | Dynamic(_,d) ->
+    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
+    else dfltpr gt
+  | gt -> dfltpr gt
+
+let wrap_exception = function
+    Anomaly (s1,s2) ->
+      warning ("Anomaly ("^s1^")"); pp s2;
+      str"<PP error: non-printable term>"
+  | Failure _ | UserError _ | Not_found ->
+      str"<PP error: non-printable term>"
+  | s -> raise s
+
+let latom = 0
+let lannot = 100
+let lprod = 200
+let llambda = 200
+let lif = 200
+let lletin = 200
+let lcases = 0
+let larrow = 90
+let lcast = 0
+let lapp = 10
+let ltop = (200,E)
+
+let prec_less child (parent,assoc) =
+  match assoc with
+  | E -> (<=) child parent
+  | L -> (<) child parent
+  | Any | Prec _ -> false
+
+let env_assoc_value v env =
+  try List.assoc v env
+  with Not_found ->
+    anomaly ("Printing metavariable "^(string_of_id v)^" is unbound")
+
+open Symbols
+
+let rec print_hunk pr env = function
+  | UnpMetaVar (e,prec) -> str "TODO" (* pr prec (env_assoc_value e env) *)
+  | UnpTerminal s -> str s
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk pr env) sub)
+  | UnpCut cut -> ppcmd_of_cut cut
+
+let pr_notation pr s env =
+  let unpl, level = find_notation_printing_rule s in
+  prlist (print_hunk pr env) unpl, level
+
+let pr_delimiters key strm =
+  let left = "`"^key^":" and right = "`" in
+  let lspace =
+    if is_letter (left.[String.length left -1]) then str " " else mt () in
+  let rspace =
+    let c = right.[0] in
+    if is_letter c or is_digit c or c = '\'' then str " " else mt () in
+  str left ++ lspace ++ strm ++ rspace ++ str right
+
+open Rawterm
+
+let pr_opt pr = function
+  | None -> mt ()
+  | Some x -> spc () ++ pr x
+
+let pr_universe u = str "<univ>"
+
+let pr_sort = function
+  | RProp Term.Null -> str "Prop"
+  | RProp Term.Pos -> str "Set"
+  | RType u -> str "Type" ++ pr_opt pr_universe u
+
+let pr_explicitation = function
+  | None -> mt ()
+  | Some n -> int n ++ str "!"
+
+let pr_expl_args pr (a,expl) =
+  pr_explicitation expl ++ pr (lapp,L) a
+
+let pr_opt_type pr = function
+  | CHole _ -> mt ()
+  | t -> cut () ++ str ":" ++ pr ltop t
+
+let pr_tight_coma () = str "," ++ cut ()
+
+let pr_name = function
+  | Anonymous -> str"_"
+  | Name id -> pr_id id
+
+let pr_located pr (loc,x) = pr x
+
+let pr_let_binder pr x a =
+  hov 0 (
+    str "let" ++ spc () ++
+    pr_name x ++ spc () ++
+    str "=" ++ spc () ++
+    pr ltop a ++ spc () ++
+    str "in")
+
+let pr_binder pr (nal,t) =
+  h 0 (
+    prlist_with_sep sep (pr_located pr_name) nal ++
+    pr_opt_type pr t)
+
+let pr_binders pr bl =
+  h 0 (prlist_with_sep sep (pr_binder pr) bl)
+
+let pr_recursive_decl pr id b t c =
+  pr_id id ++
+  brk (1,2) ++ str ": " ++ pr ltop t ++ str ":=" ++
+  brk (1,2) ++ pr ltop c
+
+let split_lambda = function
+  | CLambdaN (loc,[[na],t],c) -> (na,t,c)
+  | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+  | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let split_product = function
+  | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
+  | CProdN (loc,[[na],t],c) -> (na,t,c)
+  | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,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 (_,t,typ) = split_product typ in
+    let (bl,typ,def) = split_fix (n-1) typ def in
+    (([na],t)::bl,typ,def)
+
+let pr_fixdecl pr (id,n,t,c) =
+  let (bl,t,c) = split_fix (n+1) t c in
+  pr_recursive_decl pr id 
+    (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
+
+let pr_cofixdecl pr (id,t,c) =
+  pr_recursive_decl pr id (mt ()) t c
+
+let pr_recursive s pr_decl id = function
+  | [] -> anomaly "(co)fixpoint with no definition"
+  | d1::dl ->
+      hov 0 (
+	str "Fix " ++ pr_id id ++ brk (0,2) ++ str "{" ++
+	(v 0 (
+	  (hov 0 (pr_decl d1)) ++
+	  (prlist (fun fix -> fnl () ++ hov 0 (str "with" ++ pr_decl fix))
+	    dl))) ++
+	str "}")
+
+let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr)
+let pr_cofix pr = pr_recursive "Fix" (pr_cofixdecl pr)
+
+let rec pr_arrow pr = function
+  | CArrow (_,a,b) -> pr (larrow,L) a ++ str "->" ++ pr_arrow pr b
+  | a -> pr (larrow,E) a
+
+let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">"
+
+let pr_cases _ _ _ = str "<CASES(TODO)>"
+
+let rec pr inherited a =
+  let (strm,prec) = match a with
+  | CRef r -> pr_reference r, latom
+  | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom
+  | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom
+  | CArrow _ -> h 0 (pr_arrow pr a), larrow
+  | CProdN (_,bl,a) ->
+      h 0 (
+	str "!" ++ pr_binders pr bl ++ str "." ++ spc ()  ++ pr ltop a), lprod
+  | CLambdaN (_,bl,a) ->
+      hov 0 (
+	str "fun" ++ spc () ++ pr_binders pr bl ++ spc () ++ str "=>" ++ spc () ++ pr ltop a),
+      llambda
+  | CLetIn (_,x,a,b) ->
+      h 0 (pr_let_binder pr (snd x) a ++ spc () ++ pr ltop b), lletin
+  | CAppExpl (_,f,l) ->
+      h 0 (
+	str "@" ++ pr_reference f ++
+	prlist (fun a -> spc () ++ pr (lapp,L) a) l), lapp
+  | CApp (_,a,l) ->
+      h 0 (
+	pr (lapp,E) a  ++ 
+	prlist (fun a -> spc () ++ pr_expl_args pr a) l), lapp
+  | CCases (_,po,c,eqns) ->
+      pr_cases po c eqns, lcases
+  | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
+      (* On force les parenthèses autour d'un "if" sous-terme (même si le
+	 parsing est lui plus tolérant) *)
+      hov 0 (
+	pr_opt (pr_annotation pr) po ++
+	hv 0 (
+	  str "if" ++ pr ltop c ++ spc () ++
+	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
+	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
+  | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) ->
+      hov 0 (
+	pr_opt (pr_annotation pr) po ++
+	hv 0 (
+          str "let" ++ brk (1,1) ++
+	  hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++
+	  str "=" ++ brk (1,1) ++
+	  pr ltop c ++ spc () ++
+	  str "in " ++ pr ltop b)), lletin
+  | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
+      hov 0 (
+	hov 0 (
+	pr_opt (pr_annotation pr) po ++ brk (0,2) ++
+	  hov 0 (
+	    str (if style=RegularStyle then "Case" else "match") ++ 
+	    brk (1,1) ++ pr ltop c ++ spc () ++
+	    str (if style=RegularStyle then "of" else "with") ++
+	  brk (1,3) ++
+	  hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl)) ++
+	str "end")), lcases
+  | COrderedCase (_,_,_,_,_) -> 
+      anomaly "malformed if or destructuring let"
+  | CHole _ -> str "_", latom
+  | CMeta (_,p) -> str "@" ++ int p, latom
+  | CSort (_,s) -> pr_sort s, latom
+  | CCast (_,a,b) ->
+      hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
+  | CNotation (_,s,env) -> pr_notation pr s env
+  | CNumeral (_,p) -> Bignat.pr_bigint p, latom
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
+  | CDynamic _ -> str "<dynamic>", latom
+  in
+  if prec_less prec inherited then strm
+  else str"(" ++ strm ++ str")"
+  
+let pr_constr = pr ltop
+
+let pr_pattern = pr_constr
+let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ prc c  
+
+let pr_qualid qid = str (string_of_qualid qid)
+
+open Rawterm
+
+let pr_arg pr x = spc () ++ pr x
+
+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_metanum pr = function
+  | AN x -> pr x
+  | MetaNum (_,n) -> str "?" ++ int n
+
+let pr_metaid id = str"?" ++ pr_id id
+
+let pr_red_expr (pr_constr,pr_ref) = function
+  | Red false -> str "Red"
+  | Hnf -> str "Hnf"
+  | Simpl o -> str "Simpl" ++ pr_opt (pr_occurrences pr_constr) o  
+  | Cbv f ->
+      if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
+	str "Compute"
+      else
+	hov 1 (str "Cbv" ++ spc () ++ pr_red_flag pr_ref f)
+  | Lazy f -> 
+      hov 1 (str "Lazy" ++ spc () ++ pr_red_flag pr_ref f)
+  | Unfold l ->
+      hov 1 (str "Unfold" ++
+        prlist (fun (nl,qid) ->
+	  prlist (pr_arg int) nl ++ spc () ++ pr_ref qid) l)
+  | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l)
+  | Pattern l ->
+      hov 1 (str "Pattern" ++ prlist (pr_occurrences pr_constr) l)
+        
+  | Red true -> error "Shouldn't be accessible from user"
+  | ExtraRedExpr (s,c) ->
+      hov 1 (str s ++ pr_arg pr_constr c)
+
+let rec pr_may_eval pr = function
+  | ConstrEval (r,c) ->
+      hov 0
+        (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_reference) r ++
+	 spc () ++ str "in" ++ brk (1,1) ++ pr c)
+  | ConstrContext ((_,id),c) ->
+      hov 0
+	(str "Inst " ++ brk (1,1) ++ pr_id id ++ spc () ++
+	 str "[" ++ pr c ++ str "]")
+  | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c)
+  | ConstrTerm c -> pr c
+
+(**********************************************************************)
+let constr_syntax_universe = "constr"
+(* This is starting precedence for printing constructions or tactics *)
+(* Level 9 means no parentheses except for applicative terms (at level 10) *)
+let constr_initial_prec = Some (9,Ppextend.L)
+
+let gentermpr_fail gt =
+  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
+
+let gentermpr gt =
+  try gentermpr_fail gt
+  with s -> wrap_exception s
+
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+  gentermpr (Termast.ast_of_constr at_top env t)
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
new file mode 100644
index 0000000000..1488a9d177
--- /dev/null
+++ b/translate/ppconstrnew.mli
@@ -0,0 +1,41 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(* $Id$ *)
+
+open Pp
+open Environ
+open Term
+open Libnames
+open Pcoq
+open Rawterm
+open Extend
+open Coqast
+open Topconstr
+open Names
+open Util
+
+val split_fix : int -> constr_expr -> constr_expr ->
+  (name located list * constr_expr) list * constr_expr * constr_expr
+ 
+val pr_global : global_reference -> std_ppcmds
+ 
+val gentermpr : Coqast.t -> std_ppcmds
+val gentermpr_core : bool -> env -> constr -> std_ppcmds
+ 
+val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_name : name -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
+    ('a,'b) red_expr_gen -> std_ppcmds
+ 
+val pr_sort : rawsort -> std_ppcmds
+val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds
+val pr_constr : constr_expr -> std_ppcmds
+val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
new file mode 100644
index 0000000000..1cab30aa09
--- /dev/null
+++ b/translate/pptacticnew.ml
@@ -0,0 +1,595 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Names
+open Nameops
+open Util
+open Extend
+open Ppconstr
+open Tacexpr
+open Rawterm
+open Topconstr
+open Genarg
+open Libnames
+
+(* Extensions *)
+let prtac_tab = Hashtbl.create 17
+
+let declare_extra_tactic_pprule s f g =
+  Hashtbl.add prtac_tab s (f,g)
+
+let genarg_pprule = ref Stringmap.empty
+
+let declare_extra_genarg_pprule (rawwit, f) (wit, g) =
+  let s = match unquote wit with
+    | ExtraArgType s -> s 
+    | _ -> error
+	"Can declare a pretty-printing rule only for extra argument types"
+  in
+  let f x = f (out_gen rawwit x) in
+  let g x = g (out_gen wit x) in
+  genarg_pprule := Stringmap.add s (f,g) !genarg_pprule 
+
+(* [pr_rawtac] is here to cheat with ML typing system,
+   gen_tactic_expr is polymorphic but with some occurrences of its
+   instance raw_tactic_expr in it; then pr_tactic should be
+   polymorphic but with some calls to instance of itself, what ML does
+   not accept; pr_rawtac0 denotes this instance of pr_tactic on
+   raw_tactic_expr *)
+
+let pr_rawtac =
+  ref (fun _ -> failwith "Printer for raw tactic expr is not defined"
+       : raw_tactic_expr -> std_ppcmds)
+let pr_rawtac0 =
+  ref (fun _ -> failwith "Printer for raw tactic expr is not defined"
+       : raw_tactic_expr -> std_ppcmds)
+
+let pr_arg pr x = spc () ++ pr x
+
+let pr_metanum pr = function
+  | AN x -> pr x
+  | MetaNum (_,n) -> str "?" ++ int n
+
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (_,s) -> pr_id s
+
+let pr_or_meta pr = function
+  | AI x -> pr x
+  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"
+
+let pr_casted_open_constr = pr_constr
+
+let pr_quantified_hypothesis = function
+  | AnonHyp n -> int n
+  | NamedHyp id -> pr_id id 
+
+let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
+
+let pr_binding prc = function
+  | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
+  | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
+
+let pr_bindings prc = function
+  | ImplicitBindings l ->
+      brk (1,1) ++ str "with" ++ brk (1,1) ++
+      prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+      str"TODO" (* brk (1,1) ++ str "with" ++ brk (1,1) ++ 
+        prlist_with_sep spc (pr_binding prc) l *)
+  | NoBindings -> mt ()
+
+let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl)
+
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_id) ids ++ str "]")
+
+let rec pr_intro_pattern = function
+  | IntroOrAndPattern pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> pr_id id
+
+let pr_hyp_location pr_id = function
+  | InHyp id -> spc () ++ pr_id id
+  | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
+
+let pr_clause pr_id = function
+  | [] -> mt ()
+  | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
+
+let pr_clause_pattern pr_id = function (* To check *)
+  | (None, []) -> mt ()
+  | (glopt,l) ->
+      str "in" ++
+      prlist
+        (fun (id,nl) -> spc () ++ prlist_with_sep spc int nl 
+	  ++ spc () ++ pr_id id) l ++
+        pr_opt (prlist_with_sep spc int) glopt
+
+let pr_induction_arg prc = function
+  | ElimOnConstr c -> prc c
+  | ElimOnIdent (_,id) -> pr_id id
+  | ElimOnAnonHyp n -> int n
+
+let pr_match_pattern = function
+  | Term a -> pr_pattern a
+  | Subterm (None,a) -> str "[" ++ pr_pattern a ++ str "]"
+  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pattern a ++ str "]"
+
+let pr_match_hyps = function
+  | NoHypId mp -> str "_:" ++ pr_match_pattern mp
+  | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp
+
+let pr_match_rule m pr = function
+  | Pat ([],mp,t) when m ->
+      str "[" ++ pr_match_pattern mp ++ str "]"
+      ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
+  | Pat (rl,mp,t) ->
+      str "[" ++ prlist_with_sep pr_semicolon pr_match_hyps rl ++ spc () ++ 
+      str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++
+      spc () ++ str "->" ++ brk (1,2) ++ pr t
+  | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
+
+let pr_funvar = function
+  | None -> spc () ++ str "()"
+  | Some id -> spc () ++ pr_id id
+
+let pr_let_clause k pr = function
+  | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t)
+  | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)"
+
+let pr_let_clauses pr = function
+  | hd::tl ->
+      hv 0
+        (pr_let_clause "let " pr hd ++ spc () ++
+         prlist_with_sep spc (pr_let_clause "and " pr) tl)
+  | [] -> anomaly "LetIn must declare at least one binding"
+
+let pr_rec_clause pr ((_,id),(l,t)) =
+  pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t
+
+let pr_rec_clauses pr l = 
+  prlist_with_sep (fun () -> fnl () ++ str "and ") (pr_rec_clause pr) l
+
+let pr_hintbases = function
+  | None -> spc () ++ str "with *"
+  | Some [] -> mt ()
+  | Some l ->
+      spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l)
+
+let pr_autoarg_adding = function
+  | [] -> mt ()
+  | l ->
+      spc () ++ str "Adding [" ++
+        hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
+
+let pr_autoarg_destructing = function
+  | true -> spc () ++ str "Destructing"
+  | false -> mt ()
+
+let pr_autoarg_usingTDB = function
+  | true -> spc () ++ str "Using TDB"
+  | false -> mt ()
+
+let rec pr_rawgen prtac x =
+  match Genarg.genarg_tag x with
+  | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
+  | IntArgType -> pr_arg int (out_gen rawwit_int x)
+  | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x)
+  | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
+  | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
+  | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
+  | RefArgType -> pr_arg pr_reference (out_gen rawwit_ref x)
+  | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
+  | ConstrArgType -> pr_arg pr_constr (out_gen rawwit_constr x)
+  | ConstrMayEvalArgType ->
+      pr_arg (pr_may_eval pr_constr) (out_gen rawwit_constr_may_eval x)
+  | QuantHypArgType ->
+      pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
+  | RedExprArgType ->
+      pr_arg (pr_red_expr (pr_constr,pr_metanum pr_reference)) (out_gen rawwit_red_expr x)
+  | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
+  | CastedOpenConstrArgType ->
+      pr_arg pr_casted_open_constr (out_gen rawwit_casted_open_constr x)
+  | ConstrWithBindingsArgType -> 
+      pr_arg (pr_with_bindings pr_constr)
+      (out_gen rawwit_constr_with_bindings x)
+  | List0ArgType _ -> 
+      hov 0 (fold_list0 (fun x a -> pr_rawgen prtac x ++ a) x (mt()))
+  | List1ArgType _ ->
+      hov 0 (fold_list1 (fun x a -> pr_rawgen prtac x ++ a) x (mt()))
+  | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prtac) (mt()) x)
+  | PairArgType _ ->
+      hov 0
+        (fold_pair
+	  (fun a b -> pr_rawgen prtac a ++ spc () ++ pr_rawgen prtac b)
+	  x)
+  | ExtraArgType s -> 
+      try fst (Stringmap.find s !genarg_pprule) x
+      with Not_found -> str " [no printer for " ++ str s ++ str "] "
+
+let rec pr_raw_tacarg_using_rule pr_gen = function
+  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_raw_tacarg_using_rule pr_gen (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_raw_tacarg_using_rule  pr_gen (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_raw_extend prt s l =
+  try 
+    let (s,pl) = fst (Hashtbl.find prtac_tab s) l in
+    str s ++ pr_raw_tacarg_using_rule (pr_rawgen prt) (pl,l)
+  with Not_found ->
+    str "TODO(" ++ str s ++ prlist (pr_rawgen prt) l ++ str ")"
+
+open Closure
+
+let pr_evaluable_reference = function 
+  | EvalVarRef id -> pr_id id
+  | EvalConstRef sp -> pr_global (Libnames.ConstRef sp)
+
+let pr_inductive ind = pr_global (Libnames.IndRef ind)
+
+let rec pr_generic prtac x =
+  match Genarg.genarg_tag x with
+  | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false")
+  | IntArgType -> pr_arg int (out_gen wit_int x)
+  | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x)
+  | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\""
+  | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
+  | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
+  | RefArgType -> pr_arg pr_global (out_gen wit_ref x)
+  | SortArgType -> pr_arg Printer.prterm (Term.mkSort (out_gen wit_sort x))
+  | ConstrArgType -> pr_arg Printer.prterm (out_gen wit_constr x)
+  | ConstrMayEvalArgType ->
+      pr_arg Printer.prterm (out_gen wit_constr_may_eval x)
+  | QuantHypArgType ->
+      pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
+  | RedExprArgType ->
+      pr_arg (pr_red_expr (Printer.prterm,pr_evaluable_reference)) (out_gen wit_red_expr x)
+  | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
+  | CastedOpenConstrArgType ->
+      pr_arg Printer.prterm (snd (out_gen wit_casted_open_constr x))
+  | ConstrWithBindingsArgType -> 
+      pr_arg (pr_with_bindings Printer.prterm)
+      (out_gen wit_constr_with_bindings x)
+  | List0ArgType _ -> 
+      hov 0 (fold_list0 (fun x a -> pr_generic prtac x ++ a) x (mt()))
+  | List1ArgType _ ->
+      hov 0 (fold_list1 (fun x a -> pr_generic prtac x ++ a) x (mt()))
+  | OptArgType _ -> hov 0 (fold_opt (pr_generic prtac) (mt()) x)
+  | PairArgType _ ->
+      hov 0
+        (fold_pair
+	  (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b)
+	  x)
+  | ExtraArgType s -> 
+      try snd (Stringmap.find s !genarg_pprule) x
+      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+
+let rec pr_tacarg_using_rule prt = function
+  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule prt (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_generic prt a ++ pr_tacarg_using_rule prt (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_extend prt s l =
+  try 
+    let (s,pl) = snd (Hashtbl.find prtac_tab s) l in
+    str s ++ pr_tacarg_using_rule prt (pl,l)
+  with Not_found ->
+    str s ++ prlist (pr_generic prt) l
+
+let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) =
+
+let pr_bindings = pr_bindings pr_constr in
+let pr_with_bindings = pr_with_bindings pr_constr in
+let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
+let pr_constrarg c = spc () ++ pr_constr c in
+let pr_intarg n = spc () ++ int n in
+
+  (* Printing tactics as arguments *)
+let rec pr_atom0 = function
+  | TacIntroPattern [] -> str "Intros"
+  | TacIntroMove (None,None) -> str "Intro"
+  | TacAssumption -> str "Assumption"
+  | TacAnyConstructor None -> str "Constructor"
+  | TacTrivial (Some []) -> str "Trivial"
+  | TacAuto (None,Some []) -> str "Auto"
+  | TacAutoTDB None -> str "AutoTDB"
+  | TacDestructConcl -> str "DConcl"
+  | TacReflexivity -> str "Reflexivity"
+  | TacSymmetry -> str "Symmetry"
+  | t -> str "(" ++ pr_atom1 t ++ str ")"
+
+  (* Main tactic printer *)
+and pr_atom1 = function
+  | TacExtend (_,s,l) -> pr_extend !pr_rawtac s l
+  | TacAlias (s,l,_) -> pr_extend !pr_rawtac 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,None) as t -> pr_atom0 t
+  | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1
+  | TacIntroMove (ido1,Some (_,id2)) ->
+      hov 1
+      (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
+  | TacAssumption as t -> pr_atom0 t
+  | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
+  | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
+  | TacElim (cb,cbo) ->
+      hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ 
+        pr_opt pr_eliminator cbo)
+  | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c)
+  | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb)
+  | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
+  | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+  | TacMutualFix (id,n,l) ->
+      hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
+        hov 0 (str "with" ++ brk (1,1) ++
+          prlist_with_sep spc
+	    (fun (id,n,c) ->
+	      spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c)
+	  l))
+  | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido)
+  | TacMutualCofix (id,l) ->
+      hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++
+        hov 0 (str "with" ++ brk (1,1) ++
+          prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
+	  l))
+  | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
+  | TacTrueCut (None,c) -> 
+      hov 1 (str "Assert" ++ pr_arg pr_constr c)
+  | TacTrueCut (Some id,c) -> 
+      hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
+  | TacForward (false,na,c) ->
+      hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
+  | TacForward (true,na,c) ->
+      hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
+  | TacGeneralize l ->
+      hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l)
+  | TacGeneralizeDep c ->
+      hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
+      pr_constr c)
+  | TacLetTac (id,c,cl) ->
+      hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++
+        pr_constr c ++ pr_clause_pattern pr_ident cl)
+  | TacInstantiate (n,c) ->
+      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c)
+
+  (* Derived basic tactics *)
+  | TacOldInduction h ->
+      hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewInduction (h,e,ids) ->
+      hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
+        pr_opt pr_eliminator e ++ pr_with_names ids)
+  | TacOldDestruct h ->
+      hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewDestruct (h,e,ids) ->
+      hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
+        pr_opt pr_eliminator e ++ pr_with_names ids)
+  | 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_arg pr_constr c)
+  | TacDecomposeOr c ->
+      hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c)
+  | TacDecompose (l,c) ->
+      hov 1 (str "Decompose" ++ spc () ++
+        hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum pr_ind) l
+	  ++ str "]"))
+  | TacSpecialize (n,c) ->
+      hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
+  | TacLApply c -> 
+      hov 1 (str "LApply" ++ pr_constr c)
+
+  (* Automation tactics *)
+  | TacTrivial (Some []) as x -> pr_atom0 x
+  | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
+  | TacAuto (None,Some []) as x -> pr_atom0 x
+  | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db)
+  | TacAutoTDB None as x -> pr_atom0 x
+  | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
+  | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
+  | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id)
+  | TacDestructConcl as x -> pr_atom0 x
+  | TacSuperAuto (n,l,b1,b2) ->
+      hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
+             pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
+  | TacDAuto (n,p) ->
+      hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
+
+  (* Context management *)
+  | TacClear l ->
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
+  | TacClearBody l ->
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
+  | TacMove (b,(_,id1),(_,id2)) ->
+      (* Rem: only b = true is available for users *)
+      assert b;
+      hov 1
+        (str "Move" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ 
+	 str "after" ++ brk (1,1) ++ pr_id id2)
+  | TacRename ((_,id1),(_,id2)) ->
+      hov 1
+        (str "Rename" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ 
+	 str "into" ++ brk (1,1) ++ pr_id id2)
+
+  (* Constructors *)
+  | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
+  | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
+  | TacSplit l -> hov 1 (str "Split" ++ pr_bindings l)
+  | TacAnyConstructor (Some t) ->
+      hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t)
+  | TacAnyConstructor None as t -> pr_atom0 t
+  | TacConstructor (n,l) ->
+      hov 1 (str "Constructor" ++ pr_or_meta pr_intarg n ++ pr_bindings l)
+
+  (* Conversion *)  
+  | TacReduce (r,h) ->
+      hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h)
+  | TacChange (_,c,h) -> (* A Verifier *)
+      hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
+
+  (* Equivalence relations *)
+  | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x
+  | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
+
+and pr_tactic_seq_body tl = 
+  hv 0 (str "[ " ++
+        prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
+
+  (* Strictly closed atomic tactic expressions *)
+and pr0 = function
+  | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
+  | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
+  | TacId -> str "Idtac"
+  | TacFail 0 -> str "Fail"
+  | TacAtom (_,t) -> pr_atom0 t
+  | TacArg c -> pr_tacarg c
+  | t -> str "(" ++ prtac t ++ str ")"
+
+  (* Semi-closed atomic tactic expressions *)
+and pr1 = function
+  | TacAtom (_,t) -> pr_atom1 t
+  | TacFail n -> str "Fail " ++ int n
+  | t -> pr0 t
+
+  (* Orelse tactic expressions (printed as if parsed associating on the right
+     though the semantics is purely associative) *)
+and pr2 = function
+  | TacOrelse (t1,t2) ->
+      hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2)
+  | t -> pr1 t
+
+  (* Non closed prefix tactic expressions *)
+and pr3 = function
+  | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t)
+  | TacDo (n,t) -> hov 1 (str "Do " ++ int n ++ spc () ++ pr3 t)
+  | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
+  | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
+  | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
+  | t -> pr2 t
+
+and pr4 = function
+  | t -> pr3 t
+
+  (* THEN and THENS tactic expressions (printed as if parsed
+     associating on the left though the semantics is purely associative) *)
+and pr5 = function
+  | TacThens (t,tl) -> 
+      hov 1 (pr5 t ++ spc () ++ str "&" ++ spc () ++ pr_tactic_seq_body tl)
+  | TacThen (t1,t2) ->
+      hov 1 (pr5 t1 ++ spc () ++ str "&" ++ spc () ++ pr4 t2)
+  | t -> pr4 t
+
+  (* Ltac tactic expressions *)
+and pr6 = function
+  |(TacAtom _
+  | TacThen _
+  | TacThens _
+  | TacFirst _
+  | TacSolve _
+  | TacTry _
+  | TacOrelse _
+  | TacDo _
+  | TacRepeat _
+  | TacProgress _
+  | TacId
+  | TacFail _
+  | TacInfo _) as t -> pr5 t
+
+  | TacAbstract (t,None) -> str "Abstract " ++ pr6 t
+  | TacAbstract (t,Some s) -> 
+      hov 0
+       (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s)
+  | TacLetRecIn (l,t) -> 
+      hv 0
+        (str "let rec " ++ pr_rec_clauses prtac l ++
+        spc () ++ str "in" ++ fnl () ++ prtac t)
+  | TacLetIn (llc,u) ->
+      v 0
+       (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "in") ++ fnl () ++ prtac u)
+  | TacLetCut llc ->
+      pr_let_clauses pr_tacarg0
+        (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc)
+      ++ fnl ()
+  | TacMatch (t,lrul) ->
+      hov 0 (str "match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc()
+        ++ str "with"
+        ++ prlist
+	  (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule true prtac r)
+	lrul)
+  | TacMatchContext (lr,lrul) ->
+      hov 0 (
+	str (if lr then "Match Reverse Context With" else "Match Context With")
+	++ prlist
+	  (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule false prtac r)
+	lrul)
+  | TacFun (lvar,body) ->
+      hov 0 (str "fun" ++
+        prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body)
+  | TacArg c -> pr_tacarg c
+
+and pr_tacarg0 = function
+  | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
+  | MetaNumArg (_,n) -> str ("?" ^ string_of_int n )
+  | MetaIdArg (_,s) -> str ("$" ^ s)
+  | TacVoid -> str "()"
+  | Reference r -> pr_reference r
+  | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
+  | ConstrMayEval c -> pr_may_eval pr_constr c
+  | Integer n -> int n
+  | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
+
+and pr_tacarg1 = function
+  | TacCall (_,f,l) ->
+      hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
+  | Tacexp t -> !pr_rawtac t
+  | t -> pr_tacarg0 t
+
+and pr_tacarg x = pr_tacarg1 x
+
+and prtac x = pr6 x
+
+in (prtac,pr0,pr_match_rule)
+
+let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) =
+  make_pr_tac
+    (Ppconstrnew.pr_constr,
+     pr_metanum pr_reference,
+     pr_reference,
+     pr_or_meta (fun (loc,id) -> pr_id id),
+     pr_raw_extend)
+
+let _ = pr_rawtac := pr_raw_tactic
+let _ = pr_rawtac0 := pr_raw_tactic0
+
+let (pr_tactic,_,_) =
+  make_pr_tac
+    (Printer.prterm,
+     pr_evaluable_reference,
+     pr_inductive,
+     pr_id,
+     pr_extend)
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
new file mode 100644
index 0000000000..152b7e630d
--- /dev/null
+++ b/translate/pptacticnew.mli
@@ -0,0 +1,33 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(* $Id$ *)
+
+open Pp
+open Genarg
+open Tacexpr
+open Proof_type
+
+val declare_extra_genarg_pprule :
+  ('a raw_abstract_argument_type * ('a -> std_ppcmds)) ->
+  ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit
+ 
+val declare_extra_tactic_pprule :
+  string ->
+    (raw_generic_argument list ->
+      string * Egrammar.grammar_tactic_production list)
+    -> (closed_generic_argument list ->
+      string * Egrammar.grammar_tactic_production list)
+      -> unit
+ 
+val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) ->
+  (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds
+ 
+val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+ 
+val pr_tactic : Proof_type.tactic_expr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
new file mode 100644
index 0000000000..2996c0aecc
--- /dev/null
+++ b/translate/ppvernacnew.ml
@@ -0,0 +1,499 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)  
+
+open Pp
+open Names
+open Nameops
+open Nametab 
+open Util
+open Extend
+open Vernacexpr
+open Ppconstrnew
+open Pptacticnew
+open Rawterm
+open Coqast
+open Genarg
+open Pcoq
+open Ast
+open Libnames
+open Ppextend
+open Topconstr
+
+let sep = fun _ -> spc()
+let sep_p = fun _ -> str"."
+let sep_v = fun _ -> str","
+let sep_pp = fun _ -> str":"
+let sep_pv = fun _ -> str"; "
+
+let pr_located pr (loc,x) = pr x
+
+let pr_entry_prec = function
+  | Some Gramext.LeftA -> spc() ++ str"LEFTA"
+  | Some Gramext.RightA -> spc() ++ str"RIGHTA"
+  | Some Gramext.NonA -> spc() ++ str"NONA"
+  | None -> mt()
+
+let pr_metaid _ = str"<TODO>"
+let pr_metanum _ = str"<TODO>"
+
+let pr_set_entry_type = function
+  | ETIdent -> str"ident"
+  | ETReference -> str"global"
+  | ETPattern -> str"pattern"
+  | ETConstr _ | ETOther (_,_) -> mt ()
+  | ETBigint -> str"TODO"
+
+let pr_non_terminal = function
+  | NtQual (u,nt) -> str u ++ str" : " ++ str nt
+  | NtShort nt -> str nt
+
+let pr_production_item = function
+  | VNonTerm (loc,nt,Some p) -> pr_non_terminal nt ++ str"(" ++ pr_metaid p ++ str")"
+  | VNonTerm (loc,nt,None) -> pr_non_terminal nt
+  | VTerm s -> str s
+
+let pr_comment pr_c = function
+  | CommentConstr c -> pr_c c
+  | CommentString s -> str s
+  | CommentInt n -> int n
+
+let pr_in_out_modules = function
+  | SearchInside l -> str"inside" ++ spc() ++ prlist_with_sep sep pr_reference l
+  | SearchOutside [] -> str"outside"
+  | SearchOutside l -> str"outside" ++ spc() ++ prlist_with_sep sep pr_reference l
+
+let pr_search a b pr_c = match a with
+  | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ spc() ++ pr_in_out_modules b
+  | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_c c ++ spc() ++ pr_in_out_modules b
+  | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_c c ++ spc() ++ pr_in_out_modules b
+  | SearchAbout _ -> str"TODO"
+
+let pr_class_rawexpr = function
+  | FunClass -> str"FUNCLASS"
+  | SortClass -> str"SORTCLASS"
+  | RefClass qid -> pr_reference qid
+
+let pr_option_ref_value = function
+  | QualidRefValue id -> pr_reference id
+  | StringRefValue s -> qs s
+
+let pr_printoption a b = match a with
+  | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
+  | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
+
+let pr_set_option a b = 
+  let pr_opt_value = function 
+    | IntValue n -> int n
+    | StringValue s -> str s
+    | BoolValue b -> mt()
+  in pr_printoption a None ++ spc() ++ 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 db h pr_c = 
+  let db_name = function
+    | [] -> (false , mt())
+    | c1::c2 -> match c1 with
+      |	None,_ -> (false , mt())
+      |	Some name,_ -> (true , pr_id name)
+  in let opth = pr_opt_hintbases db 
+  in let pr_aux = function
+    | CRef qid -> pr_reference qid
+    | _ -> mt ()
+  in match h with
+  | HintsResolve l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Resolve" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Resolve" ++ spc() ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth)
+  | HintsImmediate l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Immediate" ++ spc() ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth)
+  | HintsUnfold l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Unfold" ++ spc() ++ prlist_with_sep sep pr_reference (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Unfold" ++ spc() ++ prlist_with_sep sep pr_reference (List.map (fun (_,y) -> y) l) ++ spc() ++ opth)
+  | HintsConstructors (n,c) -> hov 1 (str"Hint" ++ spc() ++ pr_id n ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Constructors" ++ spc() ++ pr_reference c) 
+  | HintsExtern (name,n,c,tac) -> hov 1 (str"Hint" ++ spc() ++ pr_id name ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Extern" ++ spc() ++ int n ++ spc() ++ pr_c c ++ pr_raw_tactic tac)
+ 
+let pr_with_declaration pr_c = function
+  | CWith_Definition (id,c) -> str"Definition" ++ spc() ++ pr_id id ++ str" := " ++ pr_c c
+  | CWith_Module (id,qid) -> str"Module" ++ spc() ++ pr_id id ++ str" := " ++ pr_located pr_qualid qid
+
+let rec pr_module_type pr_c = function
+  | CMTEident qid -> pr_located pr_qualid qid
+  | CMTEwith (mty,decl) -> pr_module_type pr_c mty ++ spc() ++ str"with" ++ spc() ++ pr_with_declaration pr_c decl
+
+let pr_module_vardecls pr_c (l,mty) = prlist_with_sep (fun _ -> str",") pr_id l ++ spc() ++ pr_module_type pr_c mty
+
+let pr_module_binders l pr_c = str"[" ++ prlist_with_sep (fun _ -> str";") (pr_module_vardecls pr_c) l ++ str"]"
+
+let pr_module_binders_list l pr_c = pr_module_binders l pr_c
+
+let rec pr_module_expr = function
+  | CMEident qid -> pr_located pr_qualid qid
+  | CMEapply (me1,me2) -> pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+
+let pr_opt_casted_constr pr_c = function
+  | CCast (loc,c,t) -> pr_c c ++ str":" ++ pr_c t
+  | _ as c -> pr_c c
+
+let pr_type_option pr_c = function
+  | CHole loc -> mt()
+  | _ as c -> str":" ++ pr_c c
+
+let pr_valdecls pr_c = function
+  | LocalRawAssum (na,c) -> prlist_with_sep (fun _ -> str",") (pr_located pr_name) na ++ spc() ++ pr_type_option pr_c c
+  | LocalRawDef (na,c) -> pr_located pr_name na ++ spc() ++ str":=" ++ spc() ++ pr_opt_casted_constr pr_c c
+
+let pr_binders pr_c l = match l with
+| [] -> mt()
+| _ as t -> str"(" ++ prlist_with_sep (fun _ -> str") (") (pr_valdecls pr_c) t ++ str")"
+
+let pr_onescheme (id,dep,ind,s) = pr_id id ++ spc() ++ str":=" ++ spc() ++ if dep then str"Induction for" else str"Minimality for" ++ spc() ++ pr_reference ind ++ spc() ++ str"Sort" ++ spc() ++ pr_sort s
+
+let pr_class_rawexpr = function
+  | FunClass -> str"FUNCLASS"
+  | SortClass -> str"SORTCLASS"
+  | RefClass qid -> pr_reference qid
+
+let pr_assumption_token = function
+  | (Decl_kinds.Local,Decl_kinds.Logical) -> str"Hypothesis"
+  | (Decl_kinds.Local,Decl_kinds.Definitional) -> str"Variable"
+  | (Decl_kinds.Global,Decl_kinds.Logical) -> str"Axiom"
+  | (Decl_kinds.Global,Decl_kinds.Definitional) -> str"Parameter"
+
+let pr_params pr_c (a,(b,c)) = pr_id b ++ spc() ++ if a then str":>" else str":" ++ spc() ++ pr_c c
+
+let pr_ne_params_list pr_c l = prlist_with_sep sep_pv (pr_params pr_c) l
+
+let pr_thm_token = function
+  | Decl_kinds.Theorem -> str"Theorem"
+  | Decl_kinds.Lemma -> str"Lemma"
+  | Decl_kinds.Fact -> str"Fact"
+  | Decl_kinds.Remark -> str"Remark"
+
+let pr_syntax_modifier = function
+  | SetItemLevel (l,n) -> prlist_with_sep (fun _ -> str",") str l ++ spc() ++ str"at level" ++ spc() ++ int n
+  | SetLevel n -> str"at level" ++ spc() ++ int n
+  | SetAssoc Gramext.LeftA -> str"left associativity"
+  | SetAssoc Gramext.RightA -> str"right associativity"
+  | SetAssoc Gramext.NonA -> str"no associativity"
+  | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+  | SetOnlyParsing -> str"only parsing"
+
+let pr_grammar_tactic_rule (name,(s,pil),t) = str name ++ spc() ++ str"[" ++ qs s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++ str"]" ++ spc() ++ str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]"
+
+let pr_box b = let pr_boxkind = function
+  | PpHB n -> str"h" ++ spc() ++ int n
+  | PpVB n -> str"v" ++ spc() ++ int n
+  | PpHVB n -> str"hv" ++ spc() ++ int n
+  | PpHOVB n -> str"hov" ++ spc() ++ int n
+  | PpTB -> str"t"
+in str"<" ++ pr_boxkind b ++ str">"
+ 
+let pr_paren_reln_or_extern = function
+  | None,L -> str"L"
+  | None,E -> str"E"
+  | Some pprim,Any -> qs pprim
+  | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
+  | _ -> mt()
+
+let rec pr_next_hunks = function 
+  | UNP_FNL -> str"FNL"
+  | UNP_TAB -> str"TAB"
+  | RO c -> qs c
+  | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]"
+  | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]"
+  | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]"
+  | PH (e,None,_) -> print_ast e
+  | PH (e,Some ext,pr) -> print_ast e ++ spc() ++ str":" ++ spc() ++ pr_paren_reln_or_extern (Some ext,pr)
+  | UNP_SYMBOLIC _ -> mt()
+
+let pr_unparsing u = prlist_with_sep sep pr_next_hunks u
+
+let pr_astpat a = str"<<" ++ print_ast a ++ str">>"
+
+let pr_syntax_rule (nm,s,u) = str nm ++ spc() ++ str"[" ++ pr_astpat s ++ str"]" ++ spc() ++ str"->" ++ spc() ++ pr_unparsing u
+
+let pr_syntax_entry (p,rl) = str"level" ++ spc() ++ int p ++ spc() ++ str":" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_syntax_rule rl
+
+let sep_end = str";"
+
+(**************************************)
+(* Pretty printer for vernac commands *)
+(**************************************)
+let make_pr_vernac pr_constr =
+
+let pr_constrarg c = spc () ++ pr_constr c in
+let pr_intarg n = spc () ++ int n in
+
+let rec pr_vernac = function
+  
+  (* Proof management *)
+  | VernacAbortAll -> str "Abort All"
+  | VernacRestart -> str"Restart"
+  | VernacSuspend -> str"Suspend"
+  | VernacUnfocus -> str"Unfocus"
+  | VernacGoal c -> str"Goal" ++ pr_constrarg c
+  | VernacAbort id -> str"Abort" ++ pr_opt (pr_located pr_id) id
+  | VernacResume id -> str"Resume" ++ pr_opt (pr_located pr_id) id
+  | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacFocus i -> str"Focus" ++ pr_opt int i
+  | VernacGo g -> 
+      let pr_goable = function
+	| GoTo i -> int i
+	| GoTop -> str"top"
+	| GoNext -> str"next"
+	| GoPrev -> str"prev" 
+      in str"Go" ++ spc() ++  pr_goable g
+  | VernacShow s -> 
+      let pr_showable = function
+	| ShowGoal n -> str"Show" ++ pr_opt int n
+	| ShowGoalImplicitly n -> str"Show Implicits" ++ 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")
+	| ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l
+	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l 
+      in pr_showable s
+  | VernacCheckGuard -> str"Guarded"
+  | VernacDebug b -> pr_topcmd b
+
+  (* Resetting *)
+  | VernacResetName id -> str"Reset" ++ spc() ++ pr_located pr_id id
+  | VernacResetInitial -> str"Reset Initial"
+  | VernacBack i -> if i=1 then str"Back" else str"Back" ++ 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_with_sep (fun _ -> sep_end ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
+  | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc()  ++ str s
+  | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
+  | VernacVar id -> pr_id id
+  
+  (* Syntax *) 
+  | VernacGrammar _ -> str"(* <Warning> : Grammar is replaced by Notation *)"
+  | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***)
+  | VernacSyntax (u,el) -> hov 1 (str"Syntax" ++ str u ++ prlist_with_sep (fun _ -> str";") pr_syntax_entry el) (***)
+  | VernacOpenScope sc -> str"Open Scope" ++ spc() ++ str sc
+  | VernacDelimiters (sc,key) -> str"Delimits Scope" ++ spc () ++ str sc ++ spc () ++ str key
+  | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function 
+      |	None -> str"_"
+      |	Some sc -> str sc in 
+    str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
+  | VernacInfix (a,p,s,q,_,sn) -> (* A Verifier *)
+      h 0 (str"Infix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+    | None -> mt()
+    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+  | VernacDistfix (a,p,s,q,sn) -> h 0 (str"Distfix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+    | None -> mt()
+    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+  | VernacNotation (s,c,l,opt) -> str"Notation" ++ spc() ++ qs s ++ pr_constrarg c ++ (match l with
+    | [] -> mt()
+    | _ as t -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str",") pr_syntax_modifier t ++ str")") ++ (match opt with
+      |	None -> mt()
+      |	Some sc -> spc() ++ str":" ++ spc() ++ str sc) (***)
+  | VernacSyntaxExtension (a,b) -> str"Uninterpreted Notation" ++ spc() ++ qs a ++ (match b with | [] -> mt() | _ as l -> str"(" ++ prlist_with_sep (fun _ -> str",") pr_syntax_modifier l ++ str")")
+
+  (* Gallina *)
+  | VernacDefinition (d,id,b,f,e) -> (* A verifier... *)
+      let pr_def_token = function
+      |	Decl_kinds.LCoercion -> str"Coercion Local"
+      |	Decl_kinds.GCoercion -> str"Coercion"
+      |	Decl_kinds.LDefinition -> str"Local"
+      |	Decl_kinds.GDefinition -> str"Definition"
+      |	Decl_kinds.SCanonical -> str"Canonical Structure"
+  in let pr_reduce = function
+    | None -> mt()
+    | Some r -> str"Eval" ++ spc() ++ pr_red_expr (pr_constr, fun _ -> str"TODO" (* pr_metanum pr_reference *)) r ++ spc() ++ str"in" ++ spc()
+  in let pr_binders_def = function
+    | [] -> mt ()
+    | _ as l -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str") (") (pr_valdecls pr_constr) l ++ str")"
+  in let pr_valloc (l,c) = match l with
+  | [] -> mt ()
+  | _ -> prlist_with_sep (fun _ -> str",") (pr_located pr_name) l ++ str":" ++ pr_constr c
+  in let pr_binders_def2 = function
+    | [] -> mt ()
+    | _ as l -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str") (") pr_valloc l ++ str")"
+  in let pr_def_body = function
+    | DefineBody (bl,red,c,d) -> (match c with
+      |	CLambdaN (_,bl2,a) -> (pr_binders_def bl ++ pr_binders_def2 bl2, (match d with
+      |	None -> mt()
+      |	Some t -> spc() ++ str":" ++ pr_constrarg t) , Some (pr_reduce red ++ pr_constr a))
+      |	_ -> (pr_binders_def bl , (match d with
+      |	None -> mt()
+      |	Some t -> spc() ++ str":" ++ pr_constrarg t) , Some (pr_reduce red ++ pr_constr c)))
+    | ProveBody (bl,t) -> (pr_binders_def bl , pr_constrarg t , None)
+ in let (binds,typ,c) = pr_def_body b
+ in h 0 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++ (match c with
+ | None -> mt()
+ | Some cc -> spc() ++ str":=" ++ spc() ++ cc))
+  | VernacStartTheoremProof (ki,id,(bl,c),b,d) -> hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++ (match bl with | [] -> mt() | _ -> pr_binders pr_constr bl ++ spc()) ++ str":" ++ spc() ++ pr_constr c)
+  | VernacEndProof (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_id id
+      |	Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_id id)) 
+  | VernacExactProof c -> str"Proof" ++ pr_constrarg c
+  | VernacAssumption (stre,l) -> hov 1 (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_constr l)
+  | VernacInductive (f,l) -> let pr_constructor (coe,(id,c)) = pr_id id ++ spc() ++ (if coe then str":>" else str":") ++ pr_constrarg c in
+    let pr_constructor_list l = match l with
+    | [] -> mt()
+    | _ -> fnl() ++ str"| " ++ prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_constructor l in
+    let pr_simple_binder (s,t) = pr_id s ++ str":" ++ pr_constr t in 
+    let pr_ne_simple_binders = function
+      |	[] -> mt()
+      |	_ as l -> str"(" ++ prlist_with_sep (fun _ -> str") (") pr_simple_binder l ++ str")" ++ spc() in      
+    let pr_oneind (id,indpar,s,lc) = pr_id id ++ spc() ++ pr_ne_simple_binders indpar ++ str":" ++ spc() ++ pr_constr s ++ spc() ++ str":=" ++ pr_constructor_list lc 
+  in hov 1 ((if f then str"Inductive" else str"CoInductive") ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_oneind l)
+  | VernacFixpoint recs -> let pr_fixbinder (l,c) = prlist_with_sep (fun _ -> str",") (pr_located pr_name) l ++ str":" ++ pr_constr c in   
+    let pr_fixbinders l = str"[" ++ prlist_with_sep (fun _ -> str";") pr_fixbinder l ++ str"]" in
+    let pr_onerec = function
+      |	(id,_,CProdN(_,bl,type_),CLambdaN(_,_,def)) -> pr_id id ++ spc() ++ pr_fixbinders bl ++ spc() ++ str":" ++ spc() ++ pr_constr type_ ++ spc() ++ str":=" ++ spc() ++ pr_constr def 
+      |	_ -> mt()
+    in hov 1 (str"Fixpoint" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_onerec recs)  
+  | VernacCoFixpoint corecs -> let pr_onecorec (id,c,def) = pr_id id ++ spc() ++ str":" ++ pr_constrarg c ++ spc() ++ str":=" ++ pr_constrarg def      
+    in hov 1 (str"CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_onecorec corecs)  
+  | VernacScheme l -> hov 1 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with") pr_onescheme l)
+
+  (* Gallina extensions *)
+  | VernacRecord ((oc,name),ps,s,c,fs) -> let pr_simple_binder (s,t) = pr_id s ++ str":" ++ pr_constr t in 
+    let pr_record_field = function
+      |	(oc,AssumExpr (id,t)) -> pr_id id ++ spc() ++ if oc then str":>" else str":" ++ spc() ++ pr_constr t
+      |	(oc,DefExpr(id,b,opt)) -> (match opt with
+	| Some t -> pr_id id ++ spc() ++ if oc then str":>" else str":" ++ spc() ++ pr_constr t ++ spc() ++ str":=" ++ pr_constr b
+	| None -> pr_id id ++ spc() ++ str":=" ++ pr_constr b) in
+    hov 1 (str"Record" ++ if oc then str" > " else spc() ++ pr_id name ++ spc() ++ (match ps with
+    | [] -> mt()
+    | _ as l -> str"[" ++ prlist_with_sep (fun _ -> str";") pr_simple_binder l ++ str"]") ++ spc() ++ str":" ++ spc() ++ (* pr_sort s *) str"TODO" ++ spc() ++ str":=" ++ (match c with
+      |	None -> mt()
+      |	Some sc -> pr_id sc) ++ spc() ++ str"{" ++ cut() ++ prlist_with_sep (fun _ -> str";" ++ brk(1,1)) pr_record_field fs ++ str"}")
+  | VernacBeginSection id -> h 0 (str"Section" ++ spc () ++ pr_id id)
+  | VernacEndSegment id -> h 0 (str"End" ++ spc() ++ pr_id id)
+  | VernacRequire (exp,spe,l) -> h 0 ((match exp with
+    | None -> str"Read Module"
+    | Some export -> str"Require" ++ if export then spc() ++ str"Export" else mt ()) ++ spc() ++  
+      (match spe with
+      |	None -> mt()
+      |	Some flag -> (if flag then str"Specification" else str"Implementation") ++ spc ()) ++
+	prlist_with_sep sep pr_reference l)
+  | VernacImport (f,l) -> if f then str"Export" else str"Import" ++ spc() ++ prlist_with_sep sep pr_reference l
+  | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q
+  | VernacCoercion (s,id,c1,c2) -> hov 1 (str"Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_reference 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 | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_id id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+
+  (* Modules and Module Types *)
+  | VernacDeclareModule (id,l,m1,m2) -> hov 1 (str"Module" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_constr ++ (match m1 with
+    | None -> mt()
+    | Some n1 -> str" : " ++ str"TODO" (* pr_module_type pr_constr n1 *) ) ++ (match m2 with
+      | None -> mt()
+      | Some n2 -> str" := " ++ pr_module_expr n2))
+  | VernacDeclareModuleType (id,l,m) -> hov 1 (str"Module Type" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_constr ++ (match m with
+    | None -> mt()
+    | Some n -> str" := " ++ pr_module_type pr_constr n))
+
+  (* Solving *)
+  | VernacSolve (i,tac,_) -> pr_raw_tactic tac (* A Verifier *)
+  | VernacSolveExistential (i,c) -> str"Existential" ++ spc() ++ int i ++ pr_constrarg c
+
+  (* Auxiliary file and library management *)
+  | VernacRequireFrom (exp,spe,f) -> h 0 (str"Require" ++ if exp then spc() ++ str"Export" ++ spc() else spc() ++ (match spe with
+    | None -> mt()
+    | Some false -> str"Implementation" ++ spc()
+    | Some true -> str"Specification" ++ spc ()) ++ qs f)
+  | VernacAddLoadPath (fl,s,d) -> hov 1 (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 l -> hov 1 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qs s
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition (_,l) -> (match l with
+    | [] -> mt()
+    | [(id,b)] -> hov 1 (str"Tactic Definition" ++ spc() ++ pr_located pr_id id ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic b)
+    | _ as t -> let pr_vrec_clause (id,b) = pr_located pr_id id ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic b in hov 1 (str"Recursive Tactic Definition" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"And") pr_vrec_clause t))
+  | VernacHints (dbnames,h) -> pr_hints dbnames h pr_constr
+  | VernacHintDestruct (id,loc,c,i,tac) -> hov 1 (str"HintDestruct" ++ spc() ++ pr_destruct_location loc ++ spc() ++ pr_id id ++ pr_constrarg c ++ pr_intarg i ++ spc() ++ str"[" ++ pr_raw_tactic tac ++ str"]")
+  | VernacSyntacticDefinition (id,c,None) -> hov 1 (str"Syntactic Definition" ++ spc() ++ pr_id id ++ spc() ++ str":=" ++ pr_constrarg c)
+  | VernacSyntacticDefinition (id,c,Some n) -> hov 1 (str"Syntactic Definition" ++ spc() ++ pr_id id ++ spc() ++ str":=" ++ pr_constrarg c ++ spc() ++ str"|" ++ int n)
+  | VernacDeclareImplicits (q,None) -> hov 1 (str"Implicits" ++ spc() ++ pr_reference q)
+  | VernacDeclareImplicits (q,Some l) -> hov 1 (str"Implicits" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep int l ++ str"]")
+  | VernacSetOpacity (fl,l) -> hov 1 (if fl then str"Opaque" else str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l)
+  | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments"
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> str"Unset Implicit Arguments"
+  | VernacSetOption (na,v) -> hov 1 (str"Set" ++ spc() ++ pr_set_option na v)
+  | VernacAddOption (na,l) -> hov 1 (str"Add" ++ spc() ++ pr_printoption na (Some l))
+  | VernacRemoveOption (na,l) -> hov 1 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
+  | VernacMemOption (na,l) -> hov 1 (str"Test" ++ spc() ++ pr_printoption na (Some l))
+  | VernacPrintOption na -> hov 1 (str"Test" ++ spc() ++ pr_printoption na None)
+  | VernacCheckMayEval (r,io,c) -> 
+      let pr_mayeval r c = match r with 
+      | Some r0 -> h 0 (str"Eval" ++ spc() ++ pr_red_expr (pr_constr,fun _ -> str"TODO" (*pr_metanum pr_reference *)) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c)
+      | None -> h 0 (str"Check" ++ spc() ++ pr_constr c) 
+      in pr_mayeval r c
+  | VernacGlobalCheck c -> hov 1 (str"Type" ++ pr_constrarg c)
+  | VernacPrint p -> 
+      let pr_printable = function
+	| PrintFullContext -> str"Print All"
+	| PrintSectionContext s -> str"Print Section" ++ spc() ++ pr_reference s
+	| PrintGrammar (uni,ent) -> str"Print Grammar" ++ spc() ++ str uni ++ spc() ++ str ent
+	| PrintLoadPath -> str"Print LoadPath"
+	| PrintModules -> str"Print Modules"
+	| PrintMLLoadPath -> str"Print ML Path"
+	| PrintMLModules -> str"Print ML Modules"
+	| PrintGraph -> str"Print Graph"
+	| PrintClasses -> str"Print Classes"
+	| PrintCoercions -> str"Print Coercions"
+	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
+	| PrintTables -> str"Print Tables"
+	| PrintOpaqueName qid -> str"Print Proof" ++ spc() ++ pr_reference qid
+	| PrintHintGoal -> str"Print Hint"
+	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid
+	| PrintHintDb -> str"Print Hint *"
+	| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
+	| PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt
+	| PrintName qid -> str"Print" ++ spc()  ++ pr_reference qid
+	| PrintLocalContext -> str"Print"
+	| 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
+	| PrintScope s -> str"Scope" ++ spc() ++ str s 
+      in pr_printable p
+  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr
+  | VernacLocate loc -> 
+      let pr_locate =function
+	| LocateTerm qid ->  pr_reference qid
+	| LocateFile f -> str"File" ++ spc() ++ qs f
+	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_reference qid
+      in str"Locate" ++ spc() ++ pr_locate loc
+  | VernacComments l -> hov 1 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l)
+  | VernacNop -> str"Proof"
+  
+  (* Toplevel control *)
+  | VernacToplevelControl exn -> pr_topcmd exn
+
+  (* For extension *)
+  | VernacExtend (s,c) -> hov 1 (str s ++ prlist_with_sep sep pr_constrarg (List.map (Genarg.out_gen Genarg.rawwit_constr) c))
+  | VernacV7only _ | VernacV8only _ -> mt ()
+  | VernacProof _ | VernacDefineModule _ -> str"TODO"
+in pr_vernac
+
+let pr_vernac = make_pr_vernac (Ppconstrnew.pr_constr)
+
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
new file mode 100644
index 0000000000..0e4bde50ea
--- /dev/null
+++ b/translate/ppvernacnew.mli
@@ -0,0 +1,31 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(* $Id$ *)
+
+open Pp
+open Genarg
+open Vernacexpr
+open Names
+open Nameops
+open Nametab
+open Util
+open Extend
+open Ppconstr
+open Pptactic
+open Rawterm
+open Coqast
+open Pcoq
+open Ast
+open Libnames
+open Ppextend
+open Topconstr
+
+val sep_end : std_ppcmds
+
+val pr_vernac : vernac_expr -> std_ppcmds