Imported Upstream version 8.0pl1upstream/8.0pl1

6 files changed, 3146 insertions, 0 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
new file mode 100644
index 00000000..7d2feaf2
--- /dev/null
+++ b/translate/ppconstrnew.ml
@@ -0,0 +1,958 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: ppconstrnew.ml,v 1.62.2.2 2004/07/16 20:48:17 herbelin Exp $ *)      
+
+(*i*)
+open Ast
+open Util
+open Pp
+open Nametab
+open Names
+open Nameops
+open Libnames
+open Coqast
+open Ppextend
+open Topconstr
+open Term
+open Pattern
+(*i*)
+
+let pr_id id = Nameops.pr_id (Constrextern.v7_to_v8_id id)
+
+let sep_p = fun _ -> str"."
+let sep_v = fun _ -> str"," ++ spc()
+let sep_pp = fun _ -> str":"
+let sep_bar = fun _ -> spc() ++ str"| "
+let pr_tight_coma () = str "," ++ cut ()
+
+let latom = 0
+let lannot = 100
+let lprod = 200
+let llambda = 200
+let lif = 200
+let lletin = 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 env_assoc_value v env =
+  try List.nth env (v-1)
+  with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
+
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | CApp (_,_,l) -> List.map fst l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+open Symbols
+
+let rec print_hunk n decode pr env = function
+  | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
+  | UnpListMetaVar (e,prec,sl) -> 
+      prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
+      (pr (n,prec)) (decode (env_assoc_value e env))
+  | UnpTerminal s -> str s
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
+  | UnpCut cut -> ppcmd_of_cut cut
+
+let pr_notation_gen decode pr s env =
+  let unpl, level = find_notation_printing_rule s in
+  prlist (print_hunk level decode pr env) unpl, level
+
+let pr_notation = pr_notation_gen decode_constrlist_value
+let pr_patnotation = pr_notation_gen decode_patlist_value
+
+let pr_delimiters key strm =
+  strm ++ str ("%"^key)
+
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
+let pr_located pr ((b,e),x) =
+  if Options.do_translate() && (b,e)<>dummy_loc then
+    let (b,e) = unloc (b,e) in
+    comment b ++ pr x ++ comment e
+  else pr x
+
+let pr_com_at n =
+  if Options.do_translate() && 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)
+
+open Rawterm
+
+let pr_opt pr = function
+  | None -> mt ()
+  | Some x -> spc() ++ pr x
+
+let pr_optc pr = function
+  | None -> mt ()
+  | Some x -> pr_sep_com 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_expl_args pr (a,expl) =
+  match expl with
+  | None -> pr (lapp,L) a
+  | Some (_,ExplByPos n) ->
+      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_name = function
+  | Anonymous -> str"_"
+  | Name id -> pr_id id
+
+let pr_lident (b,_ as 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
+  | Genarg.ArgArg x -> pr x
+  | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
+
+let las = lapp
+
+let rec pr_patt sep inh p =
+  let (strm,prec) = match p with
+  | 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
+  | CPatAtom (_,None) -> str "_", latom
+  | CPatAtom (_,Some r) -> pr_reference r, latom
+  | CPatNotation (_,"( _ )",[p]) ->
+      pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+  | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
+  | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
+  | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
+  in
+  let loc = cases_pattern_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) =
+  spc() ++ hov 4
+    (pr_with_comments loc
+      (str "| " ++
+      hov 0 (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 pr_binder many pr (nal,t) =
+  match t with
+  | CHole _ -> prlist_with_sep spc pr_lname nal
+  | _ ->
+    let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
+    hov 1 (if many then surround s else s)
+
+let pr_binder_among_many pr_c = function
+  | LocalRawAssum (nal,t) ->
+      pr_binder true pr_c (nal,t)
+  | LocalRawDef (na,c) ->
+      let c,topt = match c with
+        | CCast(_,c,t) -> c, t
+        | _ -> c, CHole dummy_loc in
+      hov 1 (surround
+        (pr_lname na ++ pr_opt_type pr_c topt ++
+         str":=" ++ cut() ++ pr_c c))
+
+let pr_undelimited_binders pr_c =
+  prlist_with_sep spc (pr_binder_among_many pr_c)
+
+let pr_delimited_binders kw pr_c bl =
+  let n = begin_of_binders bl in
+  match bl with
+  | [LocalRawAssum (nal,t)] ->
+      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t)
+  | LocalRawAssum _ :: _ as bdl ->
+      pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
+  | _ -> assert false
+
+let pr_let_binder pr x a =
+  hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++
+         pr_sep_com (fun () -> brk(0,1)) (pr ltop) a)
+
+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,t)::bl,c) ->
+      let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
+      LocalRawAssum (nal,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,t)::bl,c) ->
+      let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
+      LocalRawAssum (nal,t) :: bl, c
+  | c -> [], c
+    
+let pr_global vars ref =
+  (* pr_global_env vars ref *)
+  let s = string_of_qualid (Constrextern.shortest_qualid_of_v7_global vars ref) in
+  (str s)
+
+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 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
+  | CArrow (loc,t,c) -> (na',t,c)
+  | CProdN (loc,[[na],t],c) -> rename na na' t c
+  | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let merge_binders (na1,ty1) cofun (na2,ty2) codom =
+  let na =
+    match snd na1, snd na2 with
+        Anonymous, Name id ->
+          if occur_var_constr_expr id cofun then
+            failwith "avoid capture"
+          else na2
+      | Name id, Anonymous ->
+          if occur_var_constr_expr id codom then
+            failwith "avoid capture"
+          else na1
+      | Anonymous, Anonymous -> na1
+      | Name id1, Name id2 ->
+          if id1 <> id2 then failwith "not same name" else na1 in
+  let ty =
+    match ty1, ty2 with
+        CHole _, _ -> ty2
+      | _, CHole _ -> ty1
+      | _ ->
+          Constrextern.check_same_type ty1 ty2;
+          ty2 in
+  (LocalRawAssum ([na],ty), codom)
+            
+let rec strip_domain bvar cofun c =
+  match c with
+    | CArrow(loc,a,b) ->
+        merge_binders bvar cofun ((dummy_loc,Anonymous),a) b
+    | CProdN(loc,[([na],ty)],c') ->
+        merge_binders bvar cofun (na,ty) c'
+    | CProdN(loc,([na],ty)::bl,c') ->
+        merge_binders bvar cofun (na,ty) (CProdN(loc,bl,c'))
+    | CProdN(loc,(na::nal,ty)::bl,c') ->
+        merge_binders bvar cofun (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
+    | _ -> failwith "not a product"
+
+(* Note: binder sharing is lost *)
+let rec strip_domains (nal,ty) cofun c =
+  match nal with
+      [] -> assert false
+    | [na] ->
+        let bnd, c' = strip_domain (na,ty) cofun c in
+        ([bnd],None,c')
+    | na::nal ->
+        let f = CLambdaN(dummy_loc,[(nal,ty)],cofun) in
+        let bnd, c1 = strip_domain (na,ty) f c in
+        (try
+          let bl, rest, c2 = strip_domains (nal,ty) cofun c1 in
+          (bnd::bl, rest, c2)
+        with Failure _ -> ([bnd],Some (nal,ty), c1))
+
+(* Re-share binders *)
+let rec factorize_binders = function
+  | ([] | [_] as l) -> l
+  | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') ->
+      (try
+	let _ = Constrextern.check_same_type ty ty' in
+	factorize_binders (LocalRawAssum (nal@nal',ty)::l)
+      with _ ->
+	d :: factorize_binders l')
+  | d :: l -> d :: factorize_binders l
+
+(* Extract lambdas when a type constraint occurs *)
+let rec extract_def_binders c ty =
+  match c with
+    | CLambdaN(loc,bvar::lams,b) ->
+        (try
+          let f = CLambdaN(loc,lams,b) in
+          let bvar', rest, ty' = strip_domains bvar f ty in
+          let c' =
+            match rest, lams with
+                None,[] -> b
+              | None, _ -> f
+              | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
+          let (bl,c2,ty2) = extract_def_binders c' ty' in
+          (factorize_binders (bvar'@bl), c2, ty2)
+        with Failure _ ->
+          ([],c,ty))
+    | _ -> ([],c,ty)
+
+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],t)::bl,typ,def)
+
+let pr_recursive_decl pr id bl annot t c =
+  pr_id id ++ str" " ++
+  hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
+  pr_opt_type_spc pr t ++ str " :=" ++
+  pr_sep_com (fun () -> brk(1,2)) (pr ltop) c
+
+let pr_fixdecl pr (id,n,bl,t,c) =
+  let annot =
+    let ids = names_of_local_assums bl in
+    if List.length ids > 1 then 
+      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+    else mt() in
+  pr_recursive_decl pr id bl annot t c
+
+let pr_cofixdecl pr (id,bl,t,c) =
+  pr_recursive_decl pr id bl (mt()) t c
+
+let pr_recursive pr_decl id = function
+  | [] -> anomaly "(co)fixpoint with no definition"
+  | [d1] -> pr_decl d1
+  | dl ->
+      prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++
+      fnl() ++ str "for " ++ pr_id id
+
+let pr_arg pr x = spc () ++ pr x
+
+let is_var id = function
+  | CRef (Ident (_,id')) when id=id' -> true
+  | _ -> false
+
+let tm_clash = function
+  | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
+	nal
+      -> Some id
+  | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
+	nal
+      -> Some id
+  | _ -> None
+
+let pr_case_item pr (tm,(na,indnalopt)) =
+  hov 0 (pr (lcast,E) tm ++
+(*
+  (match na with
+    | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
+    | Anonymous when tm_clash (tm,indnalopt) <> None ->
+	(* hide [tm] name to avoid conflicts *)
+	spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*)
+    | _ -> mt ()) ++
+*)
+  (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
+    | Some na -> spc () ++ str "as " ++  pr_name na
+    | None -> mt ()) ++
+  (match indnalopt with
+    | None -> mt ()
+(*
+    | Some (_,ind,nal) ->
+        spc () ++ str "in " ++ 
+        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))
+*)
+    | Some t -> spc () ++ str "in " ++ pr lsimple t))
+
+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_return_type pr po = pr_case_type pr po
+
+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 rec pr sep inherited a =
+  let (strm,prec) = match a with
+  | CRef r -> pr_reference r, latom
+  | CFix (_,id,fix) ->
+      let p = hov 0 (str"fix " ++
+                pr_recursive (pr_fixdecl (pr mt)) (snd id) fix) in
+      if List.length fix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
+  | CCoFix (_,id,cofix) ->
+      let p =
+        hov 0 (str "cofix " ++
+               pr_recursive (pr_cofixdecl (pr mt)) (snd id) cofix) in
+      if List.length cofix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
+  | CArrow (_,a,b) ->
+      hov 0 (pr mt (larrow,L) a ++ str " ->" ++
+             pr (fun () ->brk(1,0)) (-larrow,E) b),
+      larrow
+  | CProdN _ ->
+      let (bl,a) = extract_prod_binders a in
+      hov 0 (
+	hov 2 (pr_delimited_binders (fun () -> str"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 (fun () -> str"fun" ++ spc())
+                 (pr mt ltop) bl) ++
+
+        str " =>" ++ 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 = Topconstr.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
+  | CCases (_,(po,rtntypopt),c,eqns) ->
+      v 0
+        (hv 0 (str "match" ++ brk (1,2) ++
+	  hov 0 (
+	    prlist_with_sep sep_v (pr_case_item (pr mt)) c
+            ++ pr_case_type (pr mt) 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_name 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
+     
+  | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle ->
+      (* 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_return_type (pr mt) 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
+  | COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle ->
+      hv 0 (
+        str "let " ++
+	hov 0 (str "(" ++
+               prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++
+               str ")" ++
+	       pr_return_type (pr mt) po ++ str " :=" ++
+               pr spc ltop c ++ str " in") ++
+        pr spc ltop b),
+      lletin
+
+  | COrderedCase (_,style,po,c,bl) ->
+      hv 0 (
+	str (if style=MatchStyle then "old_match " else "match ") ++ 
+	pr mt ltop c ++
+	pr_return_type (pr mt) po ++
+	str " with" ++ brk (1,0) ++
+	hov 0 (prlist
+          (fun b -> str "| ??? =>" ++ pr spc ltop b ++ fnl ()) bl) ++
+        str "end"),
+      latom
+  | CHole _ -> str "_", latom
+  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
+  | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
+  | CSort (_,s) -> pr_sort s, latom
+  | CCast (_,a,b) ->
+      hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
+      lcast
+  | CNotation (_,"( _ )",[t]) ->
+      pr (fun()->str"(") (max_int,L) t ++ str")", latom
+  | CNotation (_,s,env) -> pr_notation (pr mt) s env
+  | CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint
+  | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
+  | CDynamic _ -> str "<dynamic>", latom
+  in
+  let loc = constr_loc a in
+  pr_with_comments loc
+    (sep() ++ if prec_less prec inherited then strm else surround strm)
+
+let pr = pr mt
+
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_constr_expr c bl)
+      
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_constr_expr c bl)
+
+let rec strip_context n iscast t =
+  if n = 0 then
+    [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
+  else match t with
+    | CLambdaN (loc,(nal,t)::bll,c) ->
+	let n' = List.length nal in
+	if n' > n then
+	  let nal1,nal2 = list_chop n nal in
+	  [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+	else
+	let bl', c = strip_context (n-n') iscast
+	  (if bll=[] then c else CLambdaN (loc,bll,c)) in
+	LocalRawAssum (nal,t) :: bl', c 
+    | CProdN (loc,(nal,t)::bll,c) ->
+	let n' = List.length nal in
+	if n' > n then
+	  let nal1,nal2 = list_chop n nal in
+	  [LocalRawAssum (nal1,t)], CProdN (loc,(nal2,t)::bll,c)
+	else
+	let bl', c = strip_context (n-n') iscast
+	  (if bll=[] then c else CProdN (loc,bll,c)) in
+	LocalRawAssum (nal,t) :: bl', c 
+    | CArrow (loc,t,c) ->
+	let bl', c = strip_context (n-1) iscast c in
+	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
+    | CCast (_,c,_) -> strip_context n false c
+    | CLetIn (_,na,b,c) -> 
+	let bl', c = strip_context (n-1) iscast c in
+	LocalRawDef (na,b) :: bl', c
+    | _ -> anomaly "ppconstrnew: strip_context"
+
+let transf istype env iscast bl c =
+  let c' =
+    if istype then prod_constr_expr c bl
+    else abstract_constr_expr c bl in
+  if Options.do_translate() then
+    let r = 
+      Constrintern.for_grammar
+        (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
+	c' in
+    begin try
+      (* Try to infer old case and type annotations *)
+      let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
+      (*msgerrnl (str "Typage OK");*) ()
+    with e -> (*msgerrnl (str "Warning: can't type")*) () end;
+    let c =
+      (if istype then Constrextern.extern_rawtype
+      else Constrextern.extern_rawconstr)
+      (Termops.vars_of_env env) r in
+    let n = local_binders_length bl in
+    strip_context n iscast c
+  else bl, c
+
+let pr_constr_env env c = pr lsimple (snd (transf false env false [] c))
+let pr_lconstr_env env c = pr ltop (snd (transf false env false [] c))
+let pr_constr c = pr_constr_env (Global.env()) c
+let pr_lconstr c = pr_lconstr_env (Global.env()) c
+
+let pr_binders = pr_undelimited_binders (pr ltop)
+
+let is_Eval_key c =
+  Options.do_translate () &
+  (let f id = let s = string_of_id id in s = "Eval" in
+  let g = function
+    | Ident(_,id) -> f id
+    | Qualid (_,qid) -> let d,id = repr_qualid qid in d = empty_dirpath & f id
+  in
+  match c with
+    | CRef ref | CApp (_,(_,CRef ref),_) when g ref -> true
+    | _ -> false)
+
+let pr_protect_eval c =
+  if is_Eval_key c then h 0 (str "(" ++ pr ltop c ++ str ")") else pr ltop c
+
+let pr_lconstr_env_n env iscast bl c =
+  let bl, c = transf false env iscast bl c in
+  bl, pr_protect_eval c
+let pr_type_env_n env bl c = pr ltop (snd (transf true env false bl c))
+let pr_type c = pr ltop (snd (transf true (Global.env()) false [] c))
+
+let transf_pattern env c =
+  if Options.do_translate() then
+    Constrextern.extern_rawconstr (Termops.vars_of_env env)
+      (Constrintern.for_grammar
+	(Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[]))
+	c)
+  else c
+
+let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c)
+
+let pr_rawconstr_env env c =
+  pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+let pr_lrawconstr_env env c =
+  pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+
+let pr_cases_pattern = pr_patt ltop
+
+let pr_pattern_occ prc = function
+    ([],c) -> prc c
+  | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
+                     hov 0 (prlist_with_sep spc int nl))
+
+let pr_unfold_occ pr_ref = function
+    ([],qid) -> pr_ref qid
+  | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
+                       hov 0 (prlist_with_sep spc int nl))
+
+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_metaid id = str"?" ++ pr_id id
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
+  | Red false -> str "red"
+  | Hnf -> str "hnf"
+  | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) 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_coma (pr_unfold_occ 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_coma (pr_pattern_occ 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 test prc prlc pr2 = function
+  | ConstrEval (r,c) ->
+      hov 0
+        (str "eval" ++ brk (1,1) ++
+         pr_red_expr (prc,prlc,pr2) 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
+
+let pr_rawconstr_env_no_translate env c =
+  pr lsimple (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+let pr_lrawconstr_env_no_translate env c =
+  pr ltop (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+
+(* Printing reference with translation *)
+
+let pr_reference r =
+  let loc = loc_of_reference r in
+  try match Nametab.extended_locate (snd (qualid_of_reference r)) with
+    | TrueGlobal ref ->
+        pr_with_comments loc
+	  (pr_reference (Constrextern.extern_reference loc Idset.empty ref))
+    | SyntacticDef kn ->
+	let is_coq_root d =
+	  let d = repr_dirpath d in
+	  d <> [] & string_of_id (list_last d) = "Coq" in
+        let dir,id = repr_path (sp_of_syntactic_definition kn) in
+	let r =
+          if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then
+	    (match Syntax_def.search_syntactic_definition loc kn with
+	      | RRef (_,ref) ->
+		  Constrextern.extern_reference dummy_loc Idset.empty ref
+              | _ -> r)
+          else r
+	in pr_with_comments loc (pr_reference r)
+  with Not_found ->
+    error_global_not_found (snd (qualid_of_reference r))
+
+(** constr printers *)
+
+let pr_term_env env  c = pr lsimple (Constrextern.extern_constr false env c)
+let pr_lterm_env env c = pr ltop    (Constrextern.extern_constr false env c)
+let pr_term  c = pr_term_env  (Global.env()) c
+let pr_lterm c = pr_lterm_env (Global.env()) c
+
+let pr_constr_pattern_env env c =
+  pr lsimple (Constrextern.extern_pattern env Termops.empty_names_context c)
+
+let pr_constr_pattern t =
+  pr lsimple
+    (Constrextern.extern_pattern (Global.env()) Termops.empty_names_context t)
+
+
+(************************************************************************)
+(* Automatic standardisation of names in Arith and ZArith by translator *)
+(* Very not robust *)
+
+let is_to_rename dir id =
+  let dirs = List.map string_of_id (repr_dirpath dir) in
+  match List.rev dirs with
+  | "Coq"::"Arith"::"Between"::_ -> false
+  | "Coq"::"ZArith"::
+    ("Wf_Z"|"Zpower"|"Zlogarithm"|"Zbinary"|"Zdiv"|"Znumtheory")::_ -> false
+  | "Coq"::("Arith"|"NArith"|"ZArith")::_ -> true
+  | "Coq"::"Init"::"Peano"::_ -> true
+  | "Coq"::"Init"::"Logic"::_ when string_of_id id = "iff_trans" -> true
+  | "Coq"::"Reals"::"RIneq"::_ -> true
+  | _ -> false
+
+let is_ref_to_rename ref =
+  let sp = sp_of_global ref in
+  is_to_rename (dirpath sp) (basename sp)
+
+let get_name (ln,lp,lz,ll,lr,lr') id refbase n =
+  let id' = string_of_id n in
+  (match id' with
+    | "nat" -> (id_of_string (List.hd ln),(List.tl ln,lp,lz,ll,lr,lr'))
+    | "positive" -> (id_of_string (List.hd lp),(ln,List.tl lp,lz,ll,lr,lr'))
+    | "Z" -> (id_of_string (List.hd lz),(ln,lp,List.tl lz,ll,lr,lr'))
+    | "Prop" when List.mem (string_of_id id) ["a";"b";"c"] -> 
+	(* pour iff_trans *)
+	(id_of_string (List.hd ll),(ln,lp,lz,List.tl ll,lr,lr'))
+    | "R" when (* Noms r,r1,r2 *)
+	refbase = "Rle_refl" or
+	refbase = "Rlt_monotony_contra" or 
+	refbase = "Rmult_le_reg_l" or 
+	refbase = "Rle_monotony_contra" or 
+	refbase = "Rge_monotony" ->
+	(id_of_string (List.hd lr')),(ln,lp,lz,ll,lr,List.tl lr')
+    | "R" when (* Noms r1,r2,r3,r4 *)
+	List.mem (string_of_id id)
+	  ["x";"y";"x'";"y'";"z";"t";"n";"m";"a";"b";"c";"p";"q"] 
+	& refbase <> "sum_inequa_Rle_lt"
+	-> 
+	(id_of_string (List.hd lr),(ln,lp,lz,ll,List.tl lr,lr'))
+    | _ -> id,(ln,lp,lz,ll,lr,lr'))
+
+let get_name_constr names id refbase t = match kind_of_term t with
+  | Ind ind ->
+      let n = basename (sp_of_global (IndRef ind)) in
+      get_name names id refbase n
+  | Const sp ->
+      let n = basename (sp_of_global (ConstRef sp)) in
+      get_name names id refbase n
+  | Sort _ -> get_name names id refbase (id_of_string "Prop")
+  | _ -> id,names
+
+let names = 
+  (["n";"m";"p";"q"],["p";"q";"r";"s"],["n";"m";"p";"q"],["A";"B";"C"],
+   ["r1";"r2";"r3";"r4"],["r";"r1";"r2"])
+
+let znames refbase t =
+  let rec aux c names = match kind_of_term c with
+    | Prod (Name id as na,t,c) ->
+	let (id,names) = get_name_constr names id refbase t in
+	(na,id) :: aux c names
+    | Prod (Anonymous,t,c) ->
+	(Anonymous,id_of_string "ZZ") :: aux c names
+    | _ -> []
+  in aux t names
+
+let get_name_raw names id refbase t = match t with
+  | CRef(Ident (_,n)) -> get_name names id refbase n
+  | CSort _ -> get_name names id refbase (id_of_string "Prop")
+  | _ -> id,names
+
+let rename_bound_variables id0 t =
+  if is_to_rename (Lib.library_dp()) id0 then
+  let refbase = string_of_id id0 in
+  let rec aux c names subst = match c with
+    | CProdN (loc,bl,c) ->
+	let rec aux2 names subst = function
+	  | (nal,t)::bl ->
+	      let rec aux3 names subst = function
+		| (loc,Name id)::nal ->
+		    let (id',names) = get_name_raw names id refbase t in
+		    let (nal,names,subst) = aux3 names ((id,id')::subst) nal in
+		    (loc,Name id')::nal, names, subst
+		| x::nal -> 
+		    let (nal,names,subst) = aux3 names subst nal in
+		    x::nal,names,subst
+		| [] -> [],names,subst in
+	      let t = replace_vars_constr_expr subst t in
+	      let nal,names,subst = aux3 names subst nal in
+	      let bl,names,subst = aux2 names subst bl in
+	      (nal,t)::bl, names, subst
+	  | [] -> [],names,subst in
+	let bl,names,subst = aux2 names subst bl in
+	CProdN (loc,bl,aux c names subst)
+    | CArrow (loc,t,u) ->
+	let u = aux u names subst in
+	CArrow (loc,replace_vars_constr_expr subst t,u)
+    | _ -> replace_vars_constr_expr subst c
+  in aux t names []
+  else t
+
+let translate_binding kn n ebl =
+  let t = Retyping.get_type_of (Global.env()) Evd.empty (mkConst kn) in
+  let subst= znames (string_of_id (basename (sp_of_global (ConstRef kn)))) t in
+  try
+    let _,subst' = list_chop n subst in
+    List.map (function
+      | (x,NamedHyp id,c) -> (x,NamedHyp (List.assoc (Name id) subst'),c)
+      |  x -> x) ebl
+  with _ -> ebl
+
+let translate_with_bindings c bl =
+  match bl with
+  | ExplicitBindings l ->
+      let l = match c with
+	| RRef (_,(ConstRef kn as ref)) when is_ref_to_rename ref -> 
+	    translate_binding kn 0 l
+	| RApp (_,RRef (_,(ConstRef kn as ref)),args) when is_ref_to_rename ref
+	    -> translate_binding kn (List.length args) l
+	| _ ->
+	    l
+      in ExplicitBindings l
+    | x -> x
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
new file mode 100644
index 00000000..4477728c
--- /dev/null
+++ b/translate/ppconstrnew.mli
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+ 
+(* $Id: ppconstrnew.mli,v 1.16.2.1 2004/07/16 19:31:52 herbelin Exp $ *)
+
+open Pp
+open Environ
+open Term
+open Libnames
+open Pcoq
+open Rawterm
+open Extend
+open Coqast
+open Topconstr
+open Names
+open Util
+open Genarg
+
+val extract_lam_binders :
+  constr_expr -> local_binder list * constr_expr
+val extract_prod_binders :
+  constr_expr -> local_binder list * constr_expr
+val extract_def_binders :
+  constr_expr -> constr_expr ->
+  local_binder list * constr_expr * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr -> 
+  local_binder list *  constr_expr * constr_expr
+val pr_binders : local_binder list -> std_ppcmds
+
+val prec_less : int -> int * Ppextend.parenRelation -> bool
+ 
+val pr_global : Idset.t -> global_reference -> std_ppcmds
+ 
+val pr_tight_coma : unit -> std_ppcmds
+val pr_located :
+  ('a -> std_ppcmds) -> 'a located -> 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_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_id : identifier -> std_ppcmds
+val pr_name : name -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_metaid : identifier -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('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_lconstr : constr_expr -> std_ppcmds
+val pr_constr_env : env -> constr_expr -> std_ppcmds
+val pr_lconstr_env : env -> constr_expr -> std_ppcmds
+val pr_lconstr_env_n : env -> bool -> local_binder list -> constr_expr -> 
+  local_binder list * std_ppcmds
+val pr_type_env_n : env -> local_binder list -> constr_expr -> std_ppcmds
+val pr_type : constr_expr -> std_ppcmds
+val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
+val pr_may_eval :
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
+    -> std_ppcmds
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
+
+val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
+
+val pr_rawconstr_env_no_translate : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr_env_no_translate : env -> rawconstr -> std_ppcmds
+
+val pr_reference : reference -> std_ppcmds
+
+(** constr printers *)
+
+val pr_term_env : env -> constr -> std_ppcmds
+val pr_lterm_env : env -> constr -> std_ppcmds
+val pr_term : constr -> std_ppcmds
+val pr_lterm : constr -> std_ppcmds
+
+val pr_constr_pattern_env : env -> Pattern.constr_pattern -> std_ppcmds
+val pr_constr_pattern : Pattern.constr_pattern -> std_ppcmds
+
+(* To translate names in ZArith *)
+val translate_with_bindings : rawconstr -> 'a bindings -> 'a bindings
+val rename_bound_variables : identifier -> constr_expr -> constr_expr
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
new file mode 100644
index 00000000..80298c3e
--- /dev/null
+++ b/translate/pptacticnew.ml
@@ -0,0 +1,903 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: pptacticnew.ml,v 1.57.2.2 2004/07/16 19:31:52 herbelin Exp $ *)
+
+open Pp
+open Names
+open Nameops
+open Environ
+open Util
+open Extend
+open Ppextend
+open Ppconstrnew
+open Tacexpr
+open Rawterm
+open Topconstr
+open Genarg
+open Libnames
+open Pptactic
+
+let sep_v = fun _ -> str"," ++ spc()
+
+let strip_prod_binders_expr n ty =
+  let rec strip_ty acc n ty =
+    match ty with
+        Topconstr.CProdN(_,bll,a) ->
+          let nb =
+            List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
+          if nb >= n then (List.rev (bll@acc), a)
+          else strip_ty (bll@acc) (n-nb) a
+      | Topconstr.CArrow(_,a,b) ->
+          if n=1 then
+            (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
+          else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
+      | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+
+(* In v8 syntax only double quote char is escaped by repeating it *)
+let rec escape_string_v8 s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstringnew s = str ("\""^escape_string_v8 s^"\"")
+let qsnew = qstringnew
+
+let translate_v7_ltac = function
+  | "DiscrR" -> "discrR"
+  | "Sup0" -> "prove_sup0"
+  | "SupOmega" -> "omega_sup"
+  | "Sup" -> "prove_sup"
+  | "RCompute" -> "Rcompute"
+  | "IntroHypG" -> "intro_hyp_glob"
+  | "IntroHypL" -> "intro_hyp_pt"
+  | "IsDiff_pt" -> "is_diff_pt"
+  | "IsDiff_glob" -> "is_diff_glob"
+  | "IsCont_pt" -> "is_cont_pt"
+  | "IsCont_glob" -> "is_cont_glob"
+  | "RewTerm" -> "rew_term"
+  | "ConsProof" -> "deriv_proof"
+  | "SimplifyDerive" -> "simplify_derive"
+  | "Reg" -> "reg" (* ??? *)
+  | "SplitAbs" -> "split_case_Rabs"
+  | "SplitAbsolu" -> "split_Rabs"
+  | "SplitRmult" -> "split_Rmult"
+  | "CaseEqk" -> "case_eq"
+  | "SqRing" -> "ring_Rsqr"
+  | "TailSimpl" -> "tail_simpl"
+  | "CoInduction" -> "coinduction"
+  | "ElimCompare" -> "elim_compare"
+  | "CCsolve" -> "CCsolve"  (* ?? *)
+  | "ArrayAccess" -> "array_access"
+  | "MemAssoc" -> "mem_assoc"
+  | "SeekVarAux" -> "seek_var_aux"
+  | "SeekVar" -> "seek_var"
+  | "NumberAux" -> "number_aux"
+  | "Number" -> "number"
+  | "BuildVarList" -> "build_varlist"
+  | "Assoc" -> "assoc"
+  | "Remove" -> "remove"
+  | "Union" -> "union"
+  | "RawGiveMult" -> "raw_give_mult"
+  | "GiveMult" -> "give_mult"
+  | "ApplyAssoc" -> "apply_assoc"
+  | "ApplyDistrib" -> "apply_distrib"
+  | "GrepMult" -> "grep_mult"
+  | "WeakReduce" -> "weak_reduce"
+  | "Multiply" -> "multiply"
+  | "ApplyMultiply" -> "apply_multiply"
+  | "ApplyInverse" -> "apply_inverse"
+  | "StrongFail" -> "strong_fail"
+  | "InverseTestAux" -> "inverse_test_aux"
+  | "InverseTest" -> "inverse_test"
+  | "ApplySimplif" -> "apply_simplif"
+  | "Unfolds" -> "unfolds"
+  | "Reduce" -> "reduce"
+  | "Field_Gen_Aux" -> "field_gen_aux"
+  | "Field_Gen" -> "field_gen"
+  | "EvalWeakReduce" -> "eval_weak_reduce"
+  | "Field_Term" -> "field_term"
+  | "Fourier" -> "fourier" (* ou Fourier ?? *)
+  | "FourierEq" -> "fourier_eq"
+  | "S_to_plus" -> "rewrite_S_to_plus_term"
+  | "S_to_plus_eq" -> "rewrite_S_to_plus"
+  | "NatRing" -> "ring_nat"
+  | "Solve1" -> "solve1"
+  | "Solve2" -> "solve2"
+  | "Elim_eq_term" -> "elim_eq_term"
+  | "Elim_eq_Z" -> "elim_eq_Z"
+  | "Elim_eq_pos" -> "elim_eq_pos"
+  | "Elim_Zcompare" -> "elim_Zcompare"
+  | "ProveStable" -> "prove_stable"
+  | "interp_A" -> "interp_A"
+  | "InitExp" -> "init_exp"
+  | "SimplInv" -> "simpl_inv"
+  | "Map" -> "map_tactic"
+  | "BuildMonomAux" -> "build_monom_aux"
+  | "BuildMonom" -> "build_monom"
+  | "SimplMonomAux" -> "simpl_monom_aux"
+  | "SimplMonom" -> "simpl_monom"
+  | "SimplAllMonoms" -> "simpl_all_monomials"
+  | "AssocDistrib" -> "assoc_distrib"
+  | "NowShow" -> "now_show"
+  | ("subst"|"simpl"|"elim"|"destruct"|"apply"|"intro" (* ... *)) as x ->
+      let x' = x^"_" in
+      msgerrnl
+      (str ("Warning: '"^
+         x^"' is now a primitive tactic; it has been translated to '"^x'^"'"));
+      x'
+  | x -> x
+
+let id_of_ltac_v7_id id = 
+  id_of_string (translate_v7_ltac (string_of_id id))
+
+let pr_ltac_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (loc,id) ->
+      pr_with_comments loc (pr_id (id_of_ltac_v7_id id))
+
+let pr_arg pr x = spc () ++ pr x
+
+let pr_ltac_constant sp =
+  (* Source de bug: le nom le plus court n'est pas forcement correct 
+     apres renommage *)
+  let qid = Nametab.shortest_qualid_of_tactic sp in
+  let dir,id = repr_qualid qid in
+  pr_qualid (make_qualid dir (id_of_ltac_v7_id id))
+
+let pr_evaluable_reference_env env = function 
+  | EvalVarRef id -> pr_id (Constrextern.v7_to_v8_id id)
+  | EvalConstRef sp -> pr_global (Termops.vars_of_env env) (Libnames.ConstRef sp)
+
+let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind)
+
+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_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) =
+  if Options.do_translate () then
+    (* translator calls pr_with_bindings on rawconstr: we cast it! *)
+    let bl' = translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
+    hov 1 (prc c ++ pr_bindings prlc prc bl')
+  else
+    hov 1 (prc c ++ pr_bindings prlc prc bl)
+
+let pr_with_constr prc = function
+  | None -> mt ()
+  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
+(* Translator copy of pr_intro_pattern based on a translating "pr_id" *)
+let rec pr_intro_pattern = function
+  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> pr_id id
+and pr_case_intro_pattern = function
+  | [_::_ as pl] ->
+      str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar 
+        (fun l -> hov 0 (prlist_with_sep spc pr_intro_pattern l)) pll)
+      ++ str "]"
+
+let pr_with_names = function
+  | None -> mt ()
+  | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+let pr_occs pp = function
+    [] -> pp
+  | nl -> hov 1 (pp ++ spc() ++ str"at " ++
+                 hov 0 (prlist_with_sep spc int nl))
+
+let pr_hyp_location pr_id = function
+  | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
+  | id, occs, InHypTypeOnly ->
+      spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
+  | id, occs, InHypValueOnly ->
+      spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+
+let pr_hyp_location pr_id (id,occs,(hl,hl')) =
+  if !hl' <> None then pr_hyp_location pr_id (id,occs,out_some !hl')
+  else
+    (if hl = InHyp && Options.do_translate () then 
+      msgerrnl (h 0 (str "Translator warning: Unable to detect if " ++ pr_id id ++ spc () ++ str "denotes a local definition"));
+    pr_hyp_location pr_id (id,occs,hl))
+
+let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+
+let pr_simple_clause pr_id = function
+  | [] -> mt ()
+  | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+let pr_clauses pr_id = function
+    { onhyps=None; onconcl=true; concl_occs=nl } ->
+      pr_in (pr_occs (str " *") nl)
+  | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
+  | { onhyps=Some l; onconcl=true; concl_occs=nl } -> 
+      pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
+             ++ pr_occs (str" |- *") nl)
+  | { onhyps=Some l; onconcl=false } ->
+      pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
+
+let pr_clause_pattern pr_id = function
+  | (None, []) -> mt ()
+  | (glopt,l) ->
+      str " in" ++
+      prlist
+        (fun (id,nl) -> prlist (pr_arg int) nl 
+	  ++ spc () ++ pr_id id) l ++
+        pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
+
+let pr_induction_arg prc = function
+  | ElimOnConstr c -> 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_match_pattern pr_pat = function
+  | Term a -> pr_pat a
+  | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
+  | Subterm (Some id,a) ->
+      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
+
+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) ->
+      prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
+      spc () ++ 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 = function
+  | (id,None,t) ->
+      hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
+             pr (TacArg t))
+  | (id,Some c,t) ->
+      hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
+      pr c ++
+      str " :=" ++ brk (1,1) ++ pr (TacArg t))
+
+let pr_let_clauses pr = function
+  | hd::tl ->
+      hv 0
+        (pr_let_clause "let " pr hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
+  | [] -> anomaly "LetIn must declare at least one binding"
+
+let pr_rec_clause pr (id,(l,t)) =
+  hov 0
+    (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+
+let pr_rec_clauses pr l = 
+  prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
+
+let pr_seq_body pr tl =
+  hv 0 (str "[ " ++
+        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+        str " ]")
+
+let pr_as_names_force force ids (pp,ids') =
+  pr_with_names 
+    (if (!pp or force) & List.exists ((<>) (ref [])) ids'
+    then Some (IntroOrAndPattern (List.map (fun x -> !x) ids'))
+    else ids)
+
+let duplicate force nodup ids pr = function
+  | [] -> pr (pr_as_names_force force ids (ref false,[]))
+  | x::l when List.for_all (fun y -> snd x=snd y) l ->
+      pr (pr_as_names_force force ids x)
+  | l ->
+     if List.exists (fun (b,ids) -> !b) l & (force or
+	 List.exists (fun (_,ids) -> ids <> (snd (List.hd l))) (List.tl l))
+      then 
+        if nodup then begin
+          msgerrnl
+            (h 0 (str "Translator warning: Unable to enforce v7 names while translating Induction/NewDestruct/NewInduction. Names in the different branches are") ++ brk (0,0) ++
+            hov 0 (prlist_with_sep spc
+              (fun id -> hov 0 (pr_as_names_force true ids id))
+              (List.rev l)));
+          pr (pr_as_names_force force ids (ref false,[]))
+        end
+        else
+          pr_seq_body (fun x -> pr (pr_as_names_force force ids x)) (List.rev l)
+      else pr (pr_as_names_force force ids (ref false,[]))
+
+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_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_tacarg_using_rule pr_gen = function
+  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_then () = str ";"
+
+
+open Closure
+
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
+
+let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
+let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
+let pr_with_bindings env = pr_with_bindings (pr_lconstr env) (pr_constr env) in
+let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in
+let pr_constrarg env c = spc () ++ pr_constr env c in
+let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
+
+let pr_intarg n = spc () ++ int n in
+
+let pr_binder_fix env (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 env t in
+    spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+let pr_fix_tac env (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_from (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 env) bll ++ annot ++ str" :" ++
+        pr_lconstrarg env ty ++ str")") in
+(*  spc() ++
+  hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+    env c)
+*)
+let pr_cofix_tac env (id,c) =
+  hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
+
+
+  (* Printing tactics as arguments *)
+let rec pr_atom0 env = 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"
+  | t -> str "(" ++ pr_atom1 env t ++ str ")"
+
+  (* Main tactic printer *)
+and pr_atom1 env = function
+  | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
+  | TacSuperAuto _ | TacExtend (_,
+    ("GTauto"|"GIntuition"|"TSimplif"|
+     "LinearIntuition"),_) ->
+      errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
+  | TacExtend (loc,s,l) ->
+      pr_with_comments loc
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
+  | TacAlias (loc,s,l,_) ->
+      pr_with_comments loc
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s
+          (List.map snd l))
+
+  (* Basic tactics *)
+  | TacIntroPattern [] as t -> pr_atom0 env 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 env 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_lident id2)
+  | TacAssumption as t -> pr_atom0 env t
+  | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
+  | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
+  | TacElim (cb,cbo) ->
+      hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ 
+        pr_opt (pr_eliminator env) cbo)
+  | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c)
+  | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb)
+  | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
+  | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+  | TacMutualFix (id,n,l) ->
+      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
+             str"with " ++ prlist_with_sep spc (pr_fix_tac env) l)
+  | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
+  | TacMutualCofix (id,l) ->
+      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
+             str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
+  | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
+  | TacTrueCut (Anonymous,c) -> 
+      hov 1 (str "assert" ++ pr_constrarg env c)
+  | TacTrueCut (Name id,c) -> 
+      hov 1 (str "assert" ++ spc () ++
+             hov 1 (str"(" ++ pr_id id ++ str " :" ++
+                    pr_lconstrarg env c ++ str")"))
+  | TacForward (false,na,c) ->
+      hov 1 (str "assert" ++ spc () ++
+             hov 1 (str"(" ++ pr_name na ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
+  | TacForward (true,Anonymous,c) ->
+      if Options.do_translate () then
+        (* Pose was buggy and was wrongly substituted in conclusion in v7 *)
+        hov 1 (str "set" ++ pr_constrarg env c)
+      else
+        hov 1 (str "pose" ++ pr_constrarg env c)
+  | TacForward (true,Name id,c) ->
+      if Options.do_translate () then
+      hov 1 (str "set" ++ spc() ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
+      else
+      hov 1 (str "pose" ++ spc() ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
+  | TacGeneralize l ->
+      hov 1 (str "generalize" ++ spc () ++
+             prlist_with_sep spc (pr_constr env) l)
+  | TacGeneralizeDep c ->
+      hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
+             pr_constrarg env c)
+  | TacLetTac (Anonymous,c,cl) ->
+      hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl
+  | TacLetTac (Name id,c,cl) ->
+      hov 1 (str "set" ++ spc () ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")") ++
+             pr_clauses pr_ident cl)
+  | TacInstantiate (n,c,cls) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg env c ++ str ")" ++ 
+		    pr_clauses pr_ident cls))
+  (* Derived basic tactics *)
+  | TacSimpleInduction (h,l) ->
+      if List.exists (fun (pp,_) -> !pp) !l then
+        duplicate true true None (fun pnames -> 
+          hov 1 (str "induction" ++ pr_arg pr_quantified_hypothesis h ++
+          pnames)) !l
+      else
+      hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewInduction (h,e,(ids,l)) ->
+      duplicate false true ids (fun pnames ->
+      hov 1 (str "induction" ++ spc () ++
+             pr_induction_arg (pr_constr env) h ++ pnames ++
+             pr_opt (pr_eliminator env) e)) !l
+  | TacSimpleDestruct h ->
+      hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewDestruct (h,e,(ids,l)) ->
+      duplicate false true ids (fun pnames ->
+      hov 1 (str "destruct" ++ spc () ++
+             pr_induction_arg (pr_constr env) h ++ pnames ++
+             pr_opt (pr_eliminator env) e)) !l
+  | 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 env c)
+  | TacDecomposeOr c ->
+      hov 1 (str "decompose sum" ++ pr_constrarg env c)
+  | TacDecompose (l,c) ->
+      let vars = Termops.vars_of_env env in
+      hov 1 (str "decompose" ++ spc () ++
+        hov 0 (str "[" ++ prlist_with_sep spc (pr_ind vars) l
+	  ++ str "]" ++ pr_constrarg env c))
+  | TacSpecialize (n,c) ->
+      hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ pr_with_bindings env c)
+  | TacLApply c -> 
+      hov 1 (str "lapply" ++ pr_constrarg env c)
+
+  (* Automation tactics *)
+  | TacTrivial (Some []) as x -> pr_atom0 env x
+  | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db)
+  | TacAuto (None,Some []) as x -> pr_atom0 env x
+  | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db)
+(*  | TacAutoTDB None as x -> pr_atom0 env x
+  | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
+  | TacDestructHyp (true,id) ->
+      hov 0 (str "cdhyp" ++ spc () ++ pr_lident id)
+  | TacDestructHyp (false,id) ->
+      hov 0 (str "dhyp" ++ spc () ++ pr_lident id)
+  | TacDestructConcl as x -> pr_atom0 env 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_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 ++ spc () ++ 
+	 str "after" ++ brk (1,1) ++ pr_ident id2)
+  | TacRename (id1,id2) ->
+      hov 1
+        (str "rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
+	 str "into" ++ brk (1,1) ++ pr_ident id2)
+
+  (* Constructors *)
+  | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l)
+  | TacRight l -> hov 1 (str "right" ++ pr_bindings env l)
+  | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l)
+  | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l)
+  | TacAnyConstructor (Some t) ->
+      hov 1 (str "constructor" ++ pr_arg (pr_tac0 env) t)
+  | TacAnyConstructor None as t -> pr_atom0 env t
+  | TacConstructor (n,l) ->
+      hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++
+             pr_bindings env l)
+
+  (* Conversion *)  
+  | TacReduce (r,h) ->
+      hov 1 (pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) r ++
+             pr_clauses pr_ident h)
+  | TacChange (occ,c,h) ->
+      hov 1 (str "change" ++ brk (1,1) ++
+      (match occ with
+          None -> mt()
+        | Some([],c1) ->
+            hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
+        | Some(ocl,c1) ->
+            hov 1 (pr_constr env c1 ++ spc() ++
+	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "with ") ++
+      pr_constr env c ++ pr_clauses pr_ident h)
+
+  (* Equivalence relations *)
+  | TacReflexivity as x -> pr_atom0 env x
+  | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
+  | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c
+
+  (* Equality and inversion *)
+  | TacInversion (DepInversion (k,c,ids),hyp) ->
+      hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
+      pr_quantified_hypothesis hyp ++
+      pr_with_names ids ++ pr_with_constr (pr_constr env) c)
+  | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+      hov 1 (pr_induction_kind k ++ spc () ++
+      pr_quantified_hypothesis hyp ++
+      pr_with_names ids ++ pr_simple_clause pr_ident cl)
+  | TacInversion (InversionUsing (c,cl),hyp) ->
+      hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
+      spc () ++ str "using" ++ spc () ++ pr_constr env c ++ 
+      pr_simple_clause pr_ident cl)
+
+in
+
+let ltop = (5,E) in
+let lseq = 5 in
+let ltactical = 3 in
+let lorelse = 2 in
+let llet = 1 in
+let lfun = 1 in
+let labstract = 3 in
+let lmatch = 1 in
+let latom = 0 in
+let lcall = 1 in
+let leval = 1 in
+let ltatom = 1 in
+
+let rec pr_tac env inherited tac =
+  let (strm,prec) = match tac with
+  | TacAbstract (t,None) ->
+      str "abstract " ++ pr_tac env (labstract,L) t, labstract
+  | TacAbstract (t,Some s) -> 
+      hov 0
+       (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++
+        str "using " ++ pr_id s),
+      labstract
+  | TacLetRecIn (l,t) -> 
+      hv 0
+        (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++
+         fnl () ++ pr_tac env (llet,E) t),
+      llet
+  | TacLetIn (llc,u) ->
+      v 0
+       (hv 0 (pr_let_clauses (pr_tac env ltop) llc
+       ++ str " in") ++
+       fnl () ++ pr_tac env (llet,E) u),
+      llet
+  | TacMatch (t,lrul) ->
+      hov 0 (str "match " ++ pr_tac env ltop t ++ str " with"
+        ++ prlist
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule true (pr_tac env ltop) pr_pat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
+  | TacMatchContext (lr,lrul) ->
+      hov 0 (
+	str (if lr then "match reverse goal with" else "match goal with")
+	++ prlist
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule false (pr_tac env ltop) pr_pat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
+  | TacFun (lvar,body) ->
+      hov 2 (str "fun" ++
+        prlist pr_funvar lvar ++ str " =>" ++ spc () ++
+        pr_tac env (lfun,E) body),
+      lfun
+  | TacThens (t,tl) -> 
+      hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++
+             pr_seq_body (pr_tac env ltop) tl),
+      lseq
+  | TacThen (t1,t2) ->
+      let pp2 =
+        (* Hook for translation names in induction/destruct *)
+        match t2 with
+          | TacAtom (_,TacSimpleInduction (h,l)) ->
+              if List.exists (fun (pp,ids) -> !pp) !l then
+                duplicate true false None (fun pnames ->
+                  hov 1 
+                  (str "induction" ++ pr_arg pr_quantified_hypothesis h ++
+                  pnames)) !l
+              else
+                hov 1
+                  (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
+          | TacAtom (_,TacNewInduction (h,e,(ids,l))) ->
+              duplicate false false ids (fun pnames -> 
+                hov 1 (str "induction" ++ spc () ++
+                pr_induction_arg (pr_constr env) h ++ pnames ++
+                pr_opt (pr_eliminator env) e)) !l
+          | TacAtom (_,TacNewDestruct (h,e,(ids,l))) ->
+              duplicate false false ids (fun pnames ->
+                hov 1 (str "destruct" ++ spc () ++
+                pr_induction_arg (pr_constr env) h ++ pnames ++
+                pr_opt (pr_eliminator env) e)) !l
+              (* end hook *)
+          | _ -> pr_tac env (lseq,L) t2 in
+      hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++ pp2),
+      lseq
+  | TacTry t ->
+      hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacDo (n,t) ->
+      hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacRepeat t ->
+      hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacProgress t ->
+      hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacInfo t ->
+      hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacOrelse (t1,t2) ->
+      hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+             pr_tac env (lorelse,E) t2),
+      lorelse
+  | TacFail (ArgArg 0,"") -> str "fail", latom
+  | TacFail (n,s) -> 
+      str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+      (if s="" then mt() else qsnew s), latom
+  | TacFirst tl ->
+      str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+  | TacSolve tl ->
+      str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+  | TacId "" -> str "idtac", latom
+  | TacId s -> str "idtac" ++ (qsnew s), latom
+  | TacAtom (loc,t) ->
+      pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
+  | TacArg(Tacexp e) -> pr_tac0 env e, latom
+  | TacArg(ConstrMayEval (ConstrTerm c)) ->
+      str "constr:" ++ pr_constr env c, latom
+  | TacArg(ConstrMayEval c) ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
+  | TacArg(Integer n) -> int n, latom
+  | TacArg(TacCall(loc,f,l)) ->
+      pr_with_comments loc
+        (hov 1 (pr_ref f ++ spc () ++
+         prlist_with_sep spc (pr_tacarg env) l)),
+      lcall
+  | TacArg a -> pr_tacarg env a, latom
+  in
+  if prec_less prec inherited then strm
+  else str"(" ++ strm ++ str")"
+
+and pr_tacarg env = function
+  | TacDynamic (loc,t) ->
+      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
+  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
+  | TacVoid -> str "()"
+  | Reference r -> pr_ref r
+  | ConstrMayEval c ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
+  | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt
+  | (TacCall _|Tacexp _|Integer _) as a ->
+      str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
+
+in ((fun env -> pr_tac env ltop),
+    (fun env -> pr_tac env (latom,E)),
+    pr_match_rule)
+
+let pi1 (a,_,_) = a
+let pi2 (_,a,_) = a
+let pi3 (_,_,a) = a
+
+let strip_prod_binders_rawterm n (ty,_) =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, (ty,None)) else
+      match ty with
+          Rawterm.RProd(loc,na,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 rec raw_printers =
+    (pr_raw_tactic, 
+     pr_raw_tactic0,
+     Ppconstrnew.pr_constr_env,
+     Ppconstrnew.pr_lconstr_env,
+     Ppconstrnew.pr_pattern,
+     (fun _ -> pr_reference),
+     (fun _ -> pr_reference),
+     pr_reference,
+     pr_or_metaid pr_lident,
+     Pptactic.pr_raw_extend,
+     strip_prod_binders_expr)
+
+and pr_raw_tactic env (t:raw_tactic_expr) =
+  pi1 (make_pr_tac raw_printers) env t
+
+and pr_raw_tactic0 env t =
+  pi2 (make_pr_tac raw_printers) env t
+
+and pr_raw_match_rule env t =
+  pi3 (make_pr_tac raw_printers) env t
+
+let pr_and_constr_expr pr (c,_) = pr c
+
+
+let rec glob_printers =
+    (pr_glob_tactic, 
+     pr_glob_tactic0,
+     (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env_no_translate env)),
+     (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env_no_translate env)),
+     (fun c -> Ppconstrnew.pr_constr_pattern_env (Global.env()) c),
+     (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
+     (fun vars -> pr_or_var (pr_inductive vars)),
+     pr_ltac_or_var (pr_located pr_ltac_constant),
+     pr_lident,
+     Pptactic.pr_glob_extend,
+     strip_prod_binders_rawterm)
+
+and pr_glob_tactic env (t:glob_tactic_expr) =
+  pi1 (make_pr_tac glob_printers) env t
+
+and pr_glob_tactic0 env t =
+  pi2 (make_pr_tac glob_printers) env t
+
+and pr_glob_match_rule env t =
+  pi3 (make_pr_tac glob_printers) env t
+
+let (pr_tactic,_,_) =
+  make_pr_tac
+    (pr_glob_tactic,
+     pr_glob_tactic0,
+     pr_term_env,
+     pr_lterm_env,
+     Ppconstrnew.pr_constr_pattern,
+     pr_evaluable_reference_env,
+     pr_inductive,
+     pr_ltac_constant,
+     pr_id,
+     Pptactic.pr_extend,
+     strip_prod_binders_constr)
+
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
new file mode 100644
index 00000000..2558413f
--- /dev/null
+++ b/translate/pptacticnew.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+ 
+(* $Id: pptacticnew.mli,v 1.6.2.1 2004/07/16 19:31:52 herbelin Exp $ *)
+
+open Pp
+open Genarg
+open Tacexpr
+open Proof_type
+open Topconstr
+open Names
+
+val qsnew : string -> std_ppcmds
+
+val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds
+ 
+val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
+
+val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds
+
+val id_of_ltac_v7_id : identifier -> identifier
+
+
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
new file mode 100644
index 00000000..246253eb
--- /dev/null
+++ b/translate/ppvernacnew.ml
@@ -0,0 +1,1123 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: ppvernacnew.ml,v 1.95.2.2 2004/07/16 20:48:17 herbelin Exp $ *)  
+
+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
+open Decl_kinds
+open Tacinterp
+
+let pr_spc_type = pr_sep_com spc pr_type
+
+let pr_lident (b,_ as 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_ltac_id id = Nameops.pr_id (id_of_ltac_v7_id id)
+
+let pr_module r =
+  let update_ref s = match r with
+    | Ident (loc,_) ->
+        Ident (loc,id_of_string s)
+    | Qualid (loc,qid) ->
+        Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in
+  let (_,dir,_) =
+    try
+      Library.locate_qualified_library (snd (qualid_of_reference r))
+    with _ -> 
+      errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r)
+  in
+  let r = match List.rev (List.map string_of_id (repr_dirpath dir)) with
+    | [ "Coq"; "Lists"; "List" ] -> update_ref "MonoList"
+    | [ "Coq"; "Lists"; "PolyList" ] -> update_ref "List"
+    | _ -> r in
+  Libnames.pr_reference r
+
+let pr_import_module =
+  (* We assume List is never imported with "Import" ... *)
+  Libnames.pr_reference
+
+let pr_reference = Ppconstrnew.pr_reference
+
+let sep_end () = str"."
+
+(* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
+(*
+let pr_raw_tactic_env l env t = 
+  Pptacticnew.pr_raw_tactic env t
+*)
+let pr_raw_tactic_env l env t = 
+  Pptacticnew.pr_glob_tactic env (Tacinterp.glob_tactic_env l env t)
+
+let pr_gen env t =
+  Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env)
+    (Ppconstrnew.pr_lconstr_env env)
+    (Pptacticnew.pr_raw_tactic env) pr_reference t
+
+let pr_raw_tactic tac =
+  pr_raw_tactic_env [] (Global.env()) tac
+
+let rec extract_signature = function
+  | [] -> []
+  | Egrammar.TacNonTerm (_,(_,t),_) :: l -> t :: extract_signature l
+  | _::l -> extract_signature l
+
+let rec match_vernac_rule tys = function
+    [] -> raise Not_found
+  | (s,pargs)::rls ->
+      if extract_signature pargs = tys then (s,pargs)
+      else match_vernac_rule tys rls
+
+let sep = fun _ -> spc()
+let sep_p = fun _ -> str"."
+let sep_v = fun _ -> str","
+let sep_v2 = fun _ -> str"," ++ spc()
+let sep_pp = fun _ -> str":"
+
+let pr_ne_sep sep pr = function
+    [] -> mt()
+  | l -> sep() ++ pr l
+
+let pr_entry_prec = function
+  | Some Gramext.LeftA -> str"LEFTA "
+  | Some Gramext.RightA -> str"RIGHTA "
+  | Some Gramext.NonA -> str"NONA "
+  | None -> mt()
+
+let pr_prec = function
+  | Some Gramext.LeftA -> str", left associativity"
+  | Some Gramext.RightA -> str", right associativity"
+  | Some Gramext.NonA -> str", no associativity"
+  | None -> mt()
+
+let pr_set_entry_type = function
+  | ETIdent -> str"ident"
+  | ETReference -> str"global"
+  | ETPattern -> str"pattern"
+  | ETConstr _ -> str"constr"
+  | ETOther (_,e) -> str e
+  | ETBigint -> str "bigint"
+  | ETConstrList _ -> failwith "Internal entry type"
+
+let pr_non_terminal = function
+  | NtQual (u,nt) -> (* no more qualified entries *) str nt
+  | NtShort "constrarg" -> str "constr"
+  | NtShort nt -> str nt
+
+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
+  | VNonTerm (loc,nt,Some p) -> pr_non_terminal nt ++ str"(" ++ pr_id (strip_meta p) ++ str")"
+  | VNonTerm (loc,nt,None) -> pr_non_terminal nt
+  | VTerm s -> qsnew s
+
+let pr_comment pr_c = function
+  | CommentConstr c -> pr_c c
+  | CommentString s -> qsnew 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 = function
+  | SearchRef r -> pr_reference r
+  | SearchString s -> qsnew s
+
+let pr_search a b pr_p = match a with
+  | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ 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 local = if local then str "Local " else str ""
+
+let pr_explanation imps = function
+  | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
+  | ExplByName id -> pr_id id
+
+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 -> qsnew 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 -> 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 pr_aux = function
+    | CAppExpl (_,(_,qid),[]) -> pr_reference qid
+    | _ -> mt () in
+  let pph =
+    match h with
+    | HintsResolve l ->
+        str "Resolve " ++
+        prlist_with_sep sep pr_c (List.map snd l)
+    | HintsImmediate l ->
+        str"Immediate" ++ spc() ++
+        prlist_with_sep sep pr_c (List.map snd l)
+    | HintsUnfold l ->
+        str "Unfold " ++
+	prlist_with_sep sep pr_reference (List.map snd l)
+    | HintsConstructors (n,c) ->
+        str"Constructors" ++ spc() ++
+        prlist_with_sep spc pr_reference c
+    | HintsExtern (name,n,c,tac) ->
+        str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++
+        spc() ++ pr_raw_tactic tac
+    | HintsDestruct(name,i,loc,c,tac) ->
+        str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++
+        hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++
+               pr_c c ++ 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_lident id ++ str" := " ++ p
+  | CWith_Module (id,qid) ->
+      str"Module" ++ spc() ++ pr_lident id ++ str" := " ++
+      pr_located pr_qualid qid
+
+let rec pr_module_type pr_c = function
+  | CMTEident qid -> spc () ++ pr_located pr_qualid qid
+  | CMTEwith (mty,decl) ->
+      let m = pr_module_type pr_c mty in
+      let p = pr_with_declaration pr_c decl in
+      m ++ spc() ++ str"with" ++ spc() ++ p
+
+let pr_of_module_type prc (mty,b) =
+  str (if b then ":" else "<:") ++
+  pr_module_type prc mty
+
+let pr_module_vardecls pr_c (idl,mty) =
+  let m = pr_module_type 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 (string_of_id id),
+       Modintern.interp_modtype (Global.env()) mty]) idl;
+  (* Builds the stream *)
+  spc() ++
+  hov 1 (str"(" ++ 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 rec pr_module_expr = function
+  | CMEident qid -> pr_located pr_qualid qid
+  | CMEapply (me1,(CMEident _ as me2)) ->
+      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,me2) ->
+      pr_module_expr me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
+
+(*
+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 -> brk(0,2) ++ str":" ++ pr_c c
+
+let without_translation f x =
+  let old = Options.do_translate () in
+  let oldv7 = !Options.v7 in
+  Options.make_translate false;
+  try let r = f x in Options.make_translate old; Options.v7:=oldv7; r
+  with e -> Options.make_translate old; Options.v7:=oldv7; raise e
+
+let pr_decl_notation prc =
+  pr_opt (fun (ntn,c,scopt) -> fnl () ++
+    str "where " ++ qsnew ntn ++ str " := " ++ without_translation prc c ++
+    pr_opt (fun sc -> str ": " ++ str sc) scopt)
+
+let pr_vbinders l =
+  hv 0 (pr_binders l)
+
+let pr_binders_arg =
+  pr_ne_sep spc pr_binders
+
+let pr_and_type_binders_arg bl =
+  let bl, _ = pr_lconstr_env_n (Global.env()) false bl (CHole dummy_loc) in
+  pr_binders_arg bl
+
+let pr_onescheme (id,dep,ind,s) =
+  hov 0 (pr_lident id ++ str" :=") ++ spc() ++
+  hov 0 ((if dep then str"Induction for" else str"Minimality for")
+  ++ spc() ++ pr_reference ind) ++ spc() ++ 
+  hov 0 (str"Sort" ++ spc() ++ pr_sort s)
+
+let begin_of_inductive = function
+    [] -> 0
+  | (_,((loc,_),_))::_ -> fst (unloc loc)
+
+let pr_class_rawexpr = function
+  | FunClass -> str"Funclass"
+  | SortClass -> str"Sortclass"
+  | RefClass qid -> pr_reference 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 translate 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 = function
+  | Theorem -> str"Theorem"
+  | Lemma -> str"Lemma"
+  | Fact -> str"Fact"
+  | Remark -> str"Remark"
+
+let pr_require_token = function
+  | Some true -> str " Export"
+  | Some false -> str " Import"
+  | None -> mt()
+
+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 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"
+  | SetFormat s -> str"format " ++ pr_located qsnew s
+
+let pr_syntax_modifiers = function
+  | [] -> mt()
+  | l -> spc() ++ 
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+
+let pr_grammar_tactic_rule (name,(s,pil),t) =
+(*
+  hov 0 (
+  (* str name ++ spc() ++ *)
+  hov 0 (str"[" ++ qsnew s ++ spc() ++
+  prlist_with_sep sep pr_production_item pil ++ str"]") ++
+  spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]"))
+*)
+  hov 2 (str "Tactic Notation" ++ spc() ++ 
+    hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
+    spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
+
+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 -> qsnew pprim
+  | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p
+  | _ -> mt()
+
+let rec pr_next_hunks = function 
+  | UNP_FNL -> str"FNL"
+  | UNP_TAB -> str"TAB"
+  | RO c -> qsnew 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 =
+  str "[ " ++ prlist_with_sep sep pr_next_hunks u ++ str " ]"
+
+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 ++ str" :" ++ fnl() ++
+  prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl
+
+let pr_vernac_solve (i,env,tac,deftac) =
+  (if i = 1 then mt() else int i ++ str ": ") ++
+  Pptacticnew.pr_glob_tactic env tac
+  ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
+      with UserError _|Stdpp.Exc_located _ -> mt())
+
+(**************************************)
+(* 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 rec pr_vernac = function
+  
+  (* Proof management *)
+  | VernacAbortAll -> str "Abort All"
+  | VernacRestart -> str"Restart"
+  | VernacSuspend -> str"Suspend"
+  | VernacUnfocus -> str"Unfocus"
+  | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
+  | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
+  | VernacResume id -> str"Resume" ++ pr_opt pr_lident 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 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")
+	| 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_lident 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 () ++ qsnew s
+  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew 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()  ++ qsnew s
+  | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
+  | VernacVar id -> pr_lident id
+  
+  (* Syntax *) 
+  | VernacGrammar _ -> 
+      msgerrnl (str"Warning : constr Grammar is discontinued; use Notation");
+      str"(* <Warning> : Grammar is replaced by Notation *)"
+  | VernacTacticGrammar l ->
+      prlist_with_sep (fun () -> sep_end() ++ fnl()) pr_grammar_tactic_rule 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) ->
+      msgerrnl (str"Warning : Syntax is discontinued; use Notation");
+      str"(* <Warning> : Syntax is discontinued" ++ 
+(*
+      fnl () ++
+      hov 1 (str"Syntax " ++ str u ++ spc() ++
+      prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
+*)
+      str " *)"
+  | VernacOpenCloseScope (local,opening,sc) ->
+      str (if opening then "Open " else "Close ") ++ pr_locality local ++
+      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_class_rawexpr cll
+  | 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 (local,(s,_),q,ov8,sn) -> (* A Verifier *)
+      let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in
+      hov 0 (hov 0 (str"Infix " ++ pr_locality local
+      ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
+      pr_syntax_modifiers mv8 ++
+      (match sn with
+    | None -> mt()
+    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+  | VernacDistfix (local,a,p,s,q,sn) ->
+      hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p
+        ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with
+    | None -> mt()
+    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+  | VernacNotation (local,c,sl,mv8,opt) ->
+      let (s,l) = match mv8 with
+          None -> fst (out_some sl), []
+        | Some ml -> ml in
+      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 qsnew s else str s'
+	else qsnew s in
+      hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
+      str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
+      (match opt with
+        | None -> mt()
+        | Some sc -> str" :" ++ spc() ++ str sc))
+  | VernacSyntaxExtension (local,sl,mv8) ->
+      let (s,l) = match mv8 with
+          None -> out_some sl
+        | Some ml -> ml in
+      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++
+      pr_syntax_modifiers l
+
+  (* Gallina *)
+  | VernacDefinition (d,id,b,f) -> (* A verifier... *)
+      let pr_def_token = function
+        | Local, Coercion -> str"Coercion Local"
+        | Global, Coercion -> str"Coercion"
+        | Local, Definition -> str"Let"
+        | Global, Definition -> str"Definition"
+        | Local, SubClass -> str"Local SubClass"
+        | Global, SubClass -> str"SubClass"
+        | Global, CanonicalStructure -> str"Canonical Structure"
+        | Local, CanonicalStructure ->
+	   anomaly "Don't know how to translate a local canonical structure" in
+      let pr_reduce = function
+        | None -> mt()
+        | Some r ->
+            str"Eval" ++ spc() ++
+            pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
+            str" in" ++ spc() in
+      let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in
+      let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in
+      let pr_def_body = function
+        | DefineBody (bl,red,c,d) ->
+            let (bl2,body,ty) = match d with
+              | None ->
+                  let bl2,body = extract_lam_binders c in
+                  (bl2,body,mt())
+              | Some ty ->
+                  let bl2,body,ty' = extract_def_binders c ty in
+                  (bl2,CCast (dummy_loc,body,ty'),
+                   spc() ++ str":" ++
+                   pr_sep_com spc
+                     (pr_type_env_n (Global.env()) (bl@bl2)) ty') in
+	    let iscast = d <> None in
+            let bindings,ppred =
+	      pr_lconstr_env_n (Global.env()) iscast (bl@bl2) body in
+            (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
+        | ProveBody (bl,t) ->
+            (pr_and_type_binders_arg bl, str" :" ++ pr_spc_type 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,id,(bl,c),b,d) ->
+      hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
+      (match bl with
+        | [] -> mt()
+        | _ -> error "Statements with local binders no longer supported")
+      ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c))
+  | 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) ->
+      hov 2
+        (pr_assumption_token (List.length l > 1) stre ++ spc() ++ 
+	 pr_ne_params_list pr_type l)
+  | VernacInductive (f,l) ->
+
+      (* Copie simplifiée de command.ml pour recalculer les implicites, *)
+      (* les notations, et le contexte d'evaluation *)
+      let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in
+      let nparams = local_binders_length lparams
+      and sigma = Evd.empty 
+      and env0 = Global.env() in
+      let (env_params,params) =
+	List.fold_left
+	  (fun (env,params) d -> match d with
+	    | LocalRawAssum (nal,t) ->
+		let t = Constrintern.interp_type sigma env t in
+		let ctx = list_map_i (fun i (_,na) -> (na,None,Term.lift i t)) 0 nal
+		in let ctx = List.rev ctx in
+		(Environ.push_rel_context ctx env, ctx@params)
+	    | LocalRawDef ((_,na),c) ->
+		let c = Constrintern.judgment_of_rawconstr sigma env c in
+		let d = (na, Some c.Environ.uj_val, c.Environ.uj_type) in
+		(Environ.push_rel d env,d::params))
+	  (env0,[]) lparams in
+
+      let (ind_env,ind_impls,arityl) =
+        List.fold_left
+          (fun (env, ind_impls, arl) ((_,recname), _, _, arityc, _) ->
+            let arity = Constrintern.interp_type sigma env_params arityc in
+	    let fullarity = Termops.it_mkProd_or_LetIn arity params in
+	    let env' = Termops.push_rel_assum (Name recname,fullarity) env in
+	    let impls = 
+	      if Impargs.is_implicit_args()
+	      then Impargs.compute_implicits false env_params fullarity
+	      else [] in
+	    (env', (recname,impls)::ind_impls, (arity::arl)))
+          (env0, [], []) l
+      in
+      let lparnames = List.map (fun (na,_,_) -> na) params in
+      let notations = 
+	List.fold_right (fun (_,ntnopt,_,_,_) l ->option_cons ntnopt l) l [] in
+      let ind_env_params = Environ.push_rel_context params ind_env in
+
+      let lparnames = List.map (fun (na,_,_) -> na) params in
+      let impl = List.map
+	(fun ((_,recname),_,_,arityc,_) ->
+	  let arity = Constrintern.interp_type sigma env_params arityc in
+	  let fullarity =
+            Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params)
+	  in
+	  let impl_in =
+	    if Impargs.is_implicit_args()
+	    then Impargs.compute_implicits false env_params fullarity
+	    else [] in
+	  let impl_out =
+	    if Impargs.is_implicit_args_out()
+	    then Impargs.compute_implicits true env_params fullarity
+	    else [] in
+	  (recname,impl_in,impl_out)) l in
+      let impls_in = List.map (fun (id,a,_) -> (id,a)) impl in
+      let impls_out = List.map (fun (id,_,a) -> (id,a)) impl in
+      Constrintern.set_temporary_implicits_in impls_in;
+      Constrextern.set_temporary_implicits_out impls_out;
+      (* Fin calcul implicites *)
+
+      let pr_constructor (coe,(id,c)) =
+        hov 2 (pr_lident id ++ str" " ++
+               (if coe then str":>" else str":") ++
+                pr_sep_com spc (pr_type_env_n ind_env_params []) c) in
+      let pr_constructor_list l = match l with
+        | [] -> mt()
+        | _ ->
+            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 in
+      let pr_oneind key (id,ntn,indpar,s,lc) =
+	hov 0 (
+          str key ++ spc() ++
+          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
+	  spc() ++ pr_type s ++ 
+	  str" :=") ++ pr_constructor_list lc ++ 
+	pr_decl_notation pr_constr ntn in
+
+      (* Copie simplifiée de command.ml pour déclarer les notations locales *)
+      List.iter (fun (df,c,scope) ->
+ 	Metasyntax.add_notation_interpretation df [] c scope) notations;
+
+      hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
+      ++ 
+      (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+
+
+  | VernacFixpoint recs ->
+
+      (* Copie simplifiée de command.ml pour recalculer les implicites *)
+      (* les notations, et le contexte d'evaluation *)
+      let sigma = Evd.empty
+      and env0 = Global.env() in
+      let notations = 
+	List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in
+      let impl = List.map
+        (fun ((recname,_, bl, arityc,_),_) -> 
+          let arity =
+            Constrintern.interp_type sigma env0
+              (prod_constr_expr arityc bl) in
+	  let impl_in =
+	    if Impargs.is_implicit_args()
+	    then Impargs.compute_implicits false env0 arity
+	    else [] in
+	  let impl_out =
+	    if Impargs.is_implicit_args_out()
+	    then Impargs.compute_implicits true env0 arity
+	    else [] in
+	  (recname,impl_in,impl_out)) recs in
+      let impls_in = List.map (fun (id,a,_) -> (id,a)) impl in
+      let impls_out = List.map (fun (id,_,a) -> (id,a)) impl in
+      Constrintern.set_temporary_implicits_in impls_in;
+      Constrextern.set_temporary_implicits_out impls_out;
+
+      (* Copie simplifiée de command.ml pour déclarer les notations locales *)
+      List.iter (fun (df,c,scope) ->
+	Metasyntax.add_notation_interpretation df [] c None) notations;
+
+      let rec_sign = 
+        List.fold_left 
+          (fun env ((recname,_,bl,arityc,_),_) -> 
+            let arity =
+              Constrintern.interp_type sigma env0
+                (prod_constr_expr arityc bl) in
+            Environ.push_named (recname,None,arity) env)
+          (Global.env()) recs in
+      
+      let name_of_binder = function
+        | LocalRawAssum (nal,_) -> nal
+        | LocalRawDef (_,_) -> [] in
+      let pr_onerec = function
+        | (id,n,bl,type_,def),ntn ->
+            let (bl',def,type_) =
+              if Options.do_translate() then extract_def_binders def type_
+              else ([],def,type_) in
+            let bl = bl @ bl' in
+            let ids = List.flatten (List.map name_of_binder bl) in
+            let name =
+              try snd (List.nth ids n)
+              with Failure _ ->
+                warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+                Anonymous in
+            let annot =
+              if List.length ids > 1 then 
+                spc() ++ str "{struct " ++ pr_name name ++ str"}"
+              else mt() in
+	    let bl,ppc =
+              pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in
+            pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
+            ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
+            ++ str" :=" ++ brk(1,1) ++ ppc ++ 
+	    pr_decl_notation pr_constr ntn
+      in
+      hov 1 (str"Fixpoint" ++ spc() ++
+        prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
+
+  | VernacCoFixpoint corecs ->
+      let pr_onecorec (id,bl,c,def) =
+        let (bl',def,c) =
+              if Options.do_translate() then extract_def_binders def c
+              else ([],def,c) in
+        let bl = bl @ bl' in
+        pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+        spc() ++ pr_type c ++
+        str" :=" ++ brk(1,1) ++ pr_lconstr def in
+      hov 1 (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)
+
+  (* Gallina extensions *)
+  | VernacRecord (b,(oc,name),ps,s,c,fs) ->
+      let pr_record_field = function
+        | (oc,AssumExpr (id,t)) ->
+            hov 1 (pr_lname id ++
+            (if oc then str" :>" else str" :") ++ spc() ++
+            pr_type t)
+        | (oc,DefExpr(id,b,opt)) -> (match opt with
+	    | Some t ->
+                hov 1 (pr_lname id ++
+                (if oc then str" :>" else str" :") ++ spc() ++
+                pr_type t ++ str" :=" ++ pr_lconstr b)
+	    | None ->
+                hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+                pr_lconstr b)) in
+      hov 2
+        (str (if b then "Record" else "Structure") ++
+         (if oc then str" > " else str" ") ++ pr_lident name ++ 
+          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ 
+	  str" := " ++
+         (match c with
+           | None -> mt()
+           | Some sc -> pr_lident sc) ++
+	spc() ++ str"{"  ++
+        hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
+  | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
+  | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
+  | VernacRequire (exp,spe,l) -> hov 2
+      (str "Require" ++ pr_require_token exp ++ spc() ++
+      (match spe with
+      |	None -> mt()
+      |	Some flag ->
+          (if flag then str"Specification" else str"Implementation") ++
+          spc ()) ++
+      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_reference q
+  | VernacCoercion (s,id,c1,c2) ->
+      hov 1 (
+	str"Coercion" ++ (match s with | Local -> spc() ++
+	  str"Local" ++ spc() | 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 | Local -> spc() ++
+	  str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ 
+	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+	spc() ++ pr_class_rawexpr c2)
+
+  (* Modules and Module Types *)
+  | VernacDefineModule (m,bl,ty,bd) ->
+      let b = pr_module_binders_list bl pr_lconstr in 
+      hov 2 (str"Module " ++ pr_lident m ++ b ++
+             pr_opt (pr_of_module_type pr_lconstr) ty ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
+  | VernacDeclareModule (id,bl,m1,m2) ->
+      let b = pr_module_binders_list bl pr_lconstr in 
+      hov 2 (str"Declare Module " ++ pr_lident id ++ b ++
+             pr_opt (pr_of_module_type pr_lconstr) m1 ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
+  | VernacDeclareModuleType (id,bl,m) ->
+      let b = pr_module_binders_list bl pr_lconstr in 
+      hov 2 (str"Module Type " ++ pr_lident id ++ b ++
+             pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
+
+  (* Solving *)
+  | VernacSolve (i,tac,deftac) ->
+      (* Normally shunted by vernac.ml *)
+      let env =
+        try snd (Pfedit.get_goal_context i)
+        with UserError _ -> Global.env() in
+      let tac = 
+	Options.with_option Options.translate_syntax 
+	  (Constrintern.for_grammar (Tacinterp.glob_tactic_env [] env)) tac in
+      pr_vernac_solve (i,env,tac,deftac)
+
+  | VernacSolveExistential (i,c) ->
+      str"Existential " ++ int i ++ pr_lconstrarg c
+
+  (* Auxiliary file and library management *)
+  | VernacRequireFrom (exp,spe,f) -> hov 2
+      (str"Require " ++ pr_require_token exp ++ spc() ++
+      (match spe with
+        | None -> mt()
+        | Some false -> str"Implementation" ++ spc()
+        | Some true -> str"Specification" ++ spc ()) ++
+      qsnew f)
+  | VernacAddLoadPath (fl,s,d) -> hov 2
+      (str"Add" ++
+       (if fl then str" Rec " else spc()) ++
+       str"LoadPath" ++ spc() ++ qsnew s ++
+       (match d with 
+         | None -> mt()
+         | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) 
+  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qsnew s
+  | VernacAddMLPath (fl,s) ->
+      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qsnew s
+  | VernacDeclareMLModule l ->
+      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qsnew l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qsnew s
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition (rc,l) ->
+      let pr_tac_body (id, body) =
+        let idl, body =
+          match body with
+	    | Tacexpr.TacFun (idl,b) -> idl,b
+            | _ -> [], body in
+        pr_located pr_ltac_id id ++ 
+	prlist (function None -> str " _"
+                       | Some id -> spc () ++ pr_id id) idl
+	++ str" :=" ++ brk(1,1) ++
+	let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in
+        pr_raw_tactic_env 
+	  (idl @ List.map snd (List.map fst l))
+	  (Global.env())
+	  body in
+      hov 1
+        (((*if !Options.p1 then
+	  (if rc then str "Recursive " else mt()) ++
+	  str "Tactic Definition " else*)
+	    (* Rec by default *) str "Ltac ") ++
+        prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
+  | VernacHints (local,dbnames,h) ->
+      pr_hints local dbnames h pr_constr pr_pattern
+  | VernacSyntacticDefinition (id,c,local,onlyparsing) ->
+      hov 2
+        (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
+         pr_constrarg c ++
+         pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
+  | VernacDeclareImplicits (q,None) ->
+      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
+  | VernacDeclareImplicits (q,Some l) ->
+      let r = Nametab.global q in
+      Impargs.declare_manual_implicits r l;
+      let imps = Impargs.implicits_of_global r in
+      hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
+             str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
+  | VernacReserve (idl,c) ->
+      hov 1 (str"Implicit Type" ++
+        str (if List.length idl > 1 then "s " else " ") ++
+        prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c)
+  | VernacSetOpacity (fl,l) ->
+      hov 1 ((if fl then str"Opaque" else str"Transparent") ++
+             spc() ++ prlist_with_sep sep pr_reference l)
+
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> 
+      str"Set Implicit Arguments" 
+      ++
+      (if !Options.translate_strict_impargs then
+	sep_end () ++ fnl () ++ str"Unset Strict Implicit"
+      else mt ())
+  | VernacUnsetOption (Goptions.SecondaryTable ("Implicit","Arguments"))
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> 
+      (if !Options.translate_strict_impargs then
+	str"Set Strict Implicit" ++ sep_end () ++ fnl ()
+      else mt ())
+      ++
+      str"Unset Implicit Arguments" 
+
+  | VernacSetOption (Goptions.SecondaryTable (a,"Implicits"),BoolValue true) ->
+      str("Set "^a^" Implicit")
+  | VernacUnsetOption (Goptions.SecondaryTable (a,"Implicits")) -> 
+      str("Unset "^a^" Implicit")
+
+  | VernacUnsetOption na ->
+      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (na,v) -> hov 2 (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_reference) 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 (out_some io) ++ str ": ") ++ 
+      pr_mayeval r c
+  | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
+  | VernacPrint p -> 
+      let pr_printable = function
+	| PrintFullContext -> str"Print All"
+	| PrintSectionContext s ->
+            str"Print Section" ++ spc() ++ Libnames.pr_reference s
+	| PrintGrammar (uni,ent) ->
+            msgerrnl (str "warning: no direct translation of Print Grammar entry"); 
+            str"Print Grammar" ++ 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 Term" ++ 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 -> assert false
+            (* 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
+	| 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_reference qid
+	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
+      in pr_printable p
+  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern
+  | VernacLocate loc -> 
+      let pr_locate =function
+	| LocateTerm qid ->  pr_reference qid
+	| LocateFile f -> str"File" ++ spc() ++ qsnew f
+	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
+	| LocateNotation s -> qsnew s
+      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
+  | VernacV7only _ -> mt()
+  | VernacV8only com -> pr_vernac com
+  | VernacProof Tacexpr.TacId _ -> str "Proof"
+  | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
+
+and pr_extend s cl =
+  let pr_arg a =
+    try pr_gen (Global.env()) a
+    with Failure _ -> str ("<error in "^s^">") in
+  try
+    (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *)
+    let s =
+      let n = String.length s in
+      if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "V7"
+      then String.sub s 0 (n-2) ^ "V8"
+      else s in
+    (* "Hint Rewrite in using" changes the order of its args in v8 !! *)
+    let cl = match s, cl with
+      | "HintRewriteV8", [a;b;c;d] -> [a;b;d;c]
+      | _ -> cl in
+    let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
+    let (hd,rl) = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+    let (pp,_) =
+      List.fold_left
+        (fun (strm,args) pi ->
+          match pi with
+              Egrammar.TacNonTerm _ -> 
+                (strm ++ pr_gen (Global.env()) (List.hd args),
+                List.tl args)
+            | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
+        (str hd,cl) rl in
+    hov 1 pp
+    ++ (if s = "Correctness" then sep_end () ++ fnl() ++ str "Proof" else mt())
+  with Not_found ->
+    hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+in pr_vernac
+
+let pr_vernac = make_pr_vernac Ppconstrnew.pr_constr Ppconstrnew.pr_lconstr
+
+let pr_vernac = function
+  | VernacRequire (_,_,[Ident(_,r)]) when
+      (* Obsolete modules *)
+      List.mem (string_of_id r)
+	["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; 
+         "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep";
+	 "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax";
+	 "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax";
+	 "Zsyntax"] ->
+      warning ("Forgetting obsolete module "^(string_of_id r));
+      mt()
+  | VernacRequire (exp,spe,[Ident(_,r)]) when
+      (* Renamed modules *)
+      List.mem (string_of_id r) ["zarith_aux";"fast_integer"] ->
+      warning ("Replacing obsolete module "^(string_of_id r)^" with ZArith");
+	(str "Require" ++ pr_require_token exp ++ spc() ++
+	(match spe with
+	  | None -> mt()
+	  | Some flag ->
+	      (if flag then str"Specification" else str"Implementation") ++
+	      spc ()) ++
+	str "ZArith.")
+  | VernacImport (false,[Libnames.Ident (_,a)]) when
+      (* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *)
+      let a = Names.string_of_id a in
+      a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt()
+  | VernacSyntax _  | VernacGrammar _ as x -> pr_vernac x
+  | VernacPrint PrintLocalContext -> 
+      warning ("\"Print.\" is discontinued");
+      mt ()
+  | x -> pr_vernac x ++ sep_end ()
+
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
new file mode 100644
index 00000000..73101a1a
--- /dev/null
+++ b/translate/ppvernacnew.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+ 
+(* $Id: ppvernacnew.mli,v 1.3.2.1 2004/07/16 19:31:52 herbelin Exp $ *)
+
+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 : unit -> std_ppcmds
+
+val pr_vernac : vernac_expr -> std_ppcmds
+
+val pr_vernac_solve : 
+  int * Environ.env * Tacexpr.glob_tactic_expr * bool -> std_ppcmds