place all pretty-printing files in new dir printing/

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

15 files changed, 0 insertions, 5115 deletions

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