Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 702 insertions, 469 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4103ea00..e6c12f4f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,69 +6,64 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *)
+(* $Id: pptactic.ml 8651 2006-03-21 21:54:43Z jforest $ *)
 
 open Pp
 open Names
 open Nameops
 open Util
-open Extend
 open Tacexpr
 open Rawterm
 open Topconstr
 open Genarg
 open Libnames
 open Pattern
+open Ppextend
+open Ppconstr
+open Printer
 
-let pr_red_expr = Ppconstr.pr_red_expr
-let pr_may_eval = Ppconstr.pr_may_eval
-let pr_sort = Ppconstr.pr_sort
-let pr_global x =
-  if Options.do_translate () then (* for pr_gen *)
-    Ppconstrnew.pr_global Idset.empty x
-  else
-    Ppconstr.pr_global Idset.empty x
-let pr_name = Ppconstr.pr_name
-let pr_opt = Ppconstr.pr_opt
-let pr_occurrences = Ppconstr.pr_occurrences
+let pr_global x = Nametab.pr_global_env Idset.empty x
 
 type grammar_terminals = string option list
 
   (* Extensions *)
-let prtac_tab_v7 = Hashtbl.create 17
 let prtac_tab = Hashtbl.create 17
 
-let declare_extra_tactic_pprule for_v8 s (tags,prods) =
-  Hashtbl.add prtac_tab_v7 (s,tags) prods;
-  if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
+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_v7 (s,tags)
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (constr_expr -> std_ppcmds) -> 
+    (constr_expr -> std_ppcmds) -> 
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (rawconstr_and_expr -> std_ppcmds) ->
+    (rawconstr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
+    (Term.constr -> std_ppcmds) -> 
+    (Term.constr -> std_ppcmds) -> 
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
 
-let genarg_pprule_v7 = ref Stringmap.empty
 let genarg_pprule = ref Stringmap.empty
 
-let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
+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 prtac x = f prc prtac (out_gen rawwit x) in
-  let g prc prtac x = g prc prtac (out_gen globwit x) in
-  let h prc prtac x = h prc prtac (out_gen wit x) in
-  genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
-  if for_v8 then
-    genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule 
+  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
 
@@ -84,14 +79,10 @@ let pr_and_short_name pr (c,_) = pr c
 
 let pr_located pr (loc,x) = pr x
 
-let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)
-
 let pr_evaluable_reference = function 
   | EvalVarRef id -> pr_id id
   | EvalConstRef sp -> pr_global (Libnames.ConstRef sp)
 
-let pr_inductive ind = pr_global (Libnames.IndRef ind)
-
 let pr_quantified_hypothesis = function
   | AnonHyp n -> int n
   | NamedHyp id -> pr_id id 
@@ -108,12 +99,7 @@ let pr_bindings prc prlc = function
       prlist_with_sep spc prc l
   | ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++ 
-        prlist_with_sep spc
-          (fun b -> if Options.do_translate () or not !Options.v7 then
-	    str"(" ++ pr_binding prlc b ++ str")" 
-	   else
-	    pr_binding prc b)
-        l
+        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | NoBindings -> mt ()
 
 let pr_bindings_no_with prc prlc = function
@@ -122,21 +108,11 @@ let pr_bindings_no_with prc prlc = function
       prlist_with_sep spc prc l
   | ExplicitBindings l ->
       brk (1,1) ++ 
-        prlist_with_sep spc
-          (fun b -> if Options.do_translate () or not !Options.v7 then
-	    str"(" ++ pr_binding prlc b ++ str")" 
-	   else
-	    pr_binding prc b)
-        l
+        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
-  if Options.do_translate () then
-    (* translator calls pr_with_bindings on rawconstr: we cast it! *)
-    let bl' = Ppconstrnew.translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
-    prc c ++ hv 0 (pr_bindings prc prlc bl')
-  else
-    prc c ++ hv 0 (pr_bindings prc prlc bl)
+  prc c ++ hv 0 (pr_bindings prc prlc bl)
 
 let pr_with_constr prc = function
   | None -> mt ()
@@ -146,109 +122,10 @@ let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
-let pr_hyp_location pr_id = function
-  | id, _, (InHyp,_) -> spc () ++ pr_id id
-  | id, _, (InHypTypeOnly,_) ->
-      spc () ++ str "(Type of " ++ pr_id id ++ str ")"
-  | id, _, _ -> error "Unsupported hyp location in v7"
-
-let pr_clause pr_id = function
-  | [] -> mt ()
-  | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
-
-
-let pr_clauses pr_id cls =
-  match cls with
-      { onhyps = Some l; onconcl = false } ->
-        spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
-    | { onhyps = Some []; onconcl = true } -> mt()
-    | _ -> error "this clause has both hypothesis and conclusion"
-
-let pr_simple_clause pr_id = function
-  | [] -> mt ()
-  | l -> spc () ++
-      hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
-
-let pr_clause_pattern pr_id cls =
-  pr_opt
-    (prlist (fun (id,occs,_) ->
-      prlist (pr_arg int) occs ++ spc () ++ pr_id id)) cls.onhyps ++
-  if cls.onconcl then
-    prlist (pr_arg int) cls.concl_occs ++ spc() ++ str"Goal"
-  else mt()
-
-let pr_subterms pr occl =
-  hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
-
-let pr_induction_arg prc = function
-  | ElimOnConstr c -> prc c
-  | ElimOnIdent (_,id) -> pr_id id
-  | ElimOnAnonHyp n -> int n
-
-let pr_induction_kind = function
-  | SimpleInversion -> str "Simple Inversion"
-  | FullInversion -> str "Inversion"
-  | FullInversionClear -> str "Inversion_clear"
-
-let pr_match_pattern pr_pat = function
-  | Term a -> pr_pat a
-  | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
-  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-
-let pr_match_hyps pr_pat = function
-  | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
-
-let pr_match_rule m pr_pat pr = function
-  | Pat ([],mp,t) when m ->
-      str "[" ++ pr_match_pattern pr_pat mp ++ str "]"
-      ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
-  | Pat (rl,mp,t) ->
-      str "[" ++ prlist_with_sep pr_semicolon
-                   (pr_match_hyps pr_pat) rl ++ spc () ++ 
-      str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "]" ++
-      spc () ++ str "->" ++ brk (1,2) ++ pr t
-  | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
-
-let pr_funvar = function
-  | None -> spc () ++ str "()"
-  | Some id -> spc () ++ pr_id id
-
-let pr_let_clause k pr = function
-  | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t)
-  | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)"
-
-let pr_let_clauses pr = function
-  | hd::tl ->
-      hv 0
-        (pr_let_clause "Let " pr hd ++
-         prlist (fun t -> spc () ++ pr_let_clause "And " pr t) tl)
-  | [] -> anomaly "LetIn must declare at least one binding"
-
-let pr_rec_clause pr ((_,id),(l,t)) =
-  pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t
-
-let pr_rec_clauses pr l = 
-  prlist_with_sep (fun () -> fnl () ++ str "And ") (pr_rec_clause pr) l
-
-let pr_hintbases = function
-  | None -> spc () ++ str "with *"
-  | Some [] -> mt ()
-  | Some l ->
-      spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l)
-
-let pr_autoarg_adding = function
-  | [] -> mt ()
-  | l ->
-      spc () ++ str "Adding [" ++
-        hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
-
-let pr_autoarg_destructing = function
-  | true -> spc () ++ str "Destructing"
-  | false -> mt ()
-
-let pr_autoarg_usingTDB = function
-  | true -> spc () ++ str "Using TDB"
-  | false -> mt ()
+let rec pr_message_token prid = function
+  | MsgString s -> qs s
+  | MsgInt n -> int n
+  | MsgIdent id -> prid id
 
 let rec pr_raw_generic prc prlc prtac prref x =
   match Genarg.genarg_tag x with
@@ -259,24 +136,20 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
   | IntroPatternArgType -> pr_arg pr_intro_pattern 
       (out_gen rawwit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen rawwit_ident x))
-  | HypArgType -> pr_arg
-      (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen rawwit_var x)
+  | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
+  | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
   | RefArgType -> pr_arg prref (out_gen rawwit_ref x)
   | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc prref)
+      pr_arg (pr_may_eval prc prlc prref)
         (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr 
-        (prc,prref)) (out_gen rawwit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
-  | CastedOpenConstrArgType ->
-      pr_arg prc (snd (out_gen rawwit_casted_open_constr x))
+      pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
+  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x)
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -293,10 +166,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
             pr_raw_generic prc prlc prtac prref b)
 	  x)
   | ExtraArgType s -> 
-      let tab =
-	if Options.do_translate() or not !Options.v7 then !genarg_pprule
-        else !genarg_pprule_v7 in
-      try pi1 (Stringmap.find s tab) prc prtac x
+      try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
 
 
@@ -309,23 +179,22 @@ let rec pr_glob_generic prc prlc prtac x =
   | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
   | IntroPatternArgType ->
       pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen globwit_ident x))
-  | HypArgType -> pr_arg (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen globwit_var x)
+  | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
+  | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
   | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
   | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc
+      pr_arg (pr_may_eval prc prlc
         (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr 
-        (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
-  | CastedOpenConstrArgType ->
-      pr_arg prc (snd (out_gen globwit_casted_open_constr x))
+        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
+        (out_gen globwit_red_expr x)
+  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x)
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -342,10 +211,7 @@ let rec pr_glob_generic prc prlc prtac x =
             pr_glob_generic prc prlc prtac b)
 	  x)
   | ExtraArgType s -> 
-      let tab =
-	if Options.do_translate() or not !Options.v7 then !genarg_pprule
-        else !genarg_pprule_v7 in
-      try pi2 (Stringmap.find s tab) prc prtac x
+      try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
 
 open Closure
@@ -359,8 +225,8 @@ let rec pr_generic prc prlc prtac x =
   | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
   | IntroPatternArgType -> 
       pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
-  | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x))
-  | HypArgType -> pr_arg prc (out_gen wit_var x)
+  | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
+  | VarArgType -> pr_arg pr_id (out_gen wit_var x)
   | RefArgType -> pr_arg pr_global (out_gen wit_ref x)
   | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
   | ConstrArgType -> pr_arg prc (out_gen wit_constr x)
@@ -369,11 +235,10 @@ let rec pr_generic prc prlc prtac x =
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
-  | CastedOpenConstrArgType ->
-      pr_arg prc (snd (out_gen wit_casted_open_constr x))
+      pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) 
+        (out_gen wit_red_expr x)
+  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x)
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -390,10 +255,7 @@ let rec pr_generic prc prlc prtac x =
             pr_generic prc prlc prtac b)
 	  x)
   | ExtraArgType s -> 
-      let tab = 
-	if Options.do_translate() or not !Options.v7 then !genarg_pprule
-        else !genarg_pprule_v7 in
-      try pi3 (Stringmap.find s tab) prc prtac x
+      try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "]"
 
 let rec pr_tacarg_using_rule pr_gen = function
@@ -402,364 +264,735 @@ let rec pr_tacarg_using_rule pr_gen = function
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_extend_gen prgen s l =
-  let tab = 
-    if Options.do_translate() or not !Options.v7 then prtac_tab
-    else prtac_tab_v7
-  in
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
+let pr_extend_gen prgen lev s l =
   try 
     let tags = List.map genarg_tag l in
-    (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *)
-    let s =
-      let n = String.length s in
-      if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "v7"
-      then String.sub s 0 (n-2) ^ "v8"
-      else s in
-    let (s,pl) = Hashtbl.find tab (s,tags) in
-    str s ++ pr_tacarg_using_rule prgen (pl,l)
+    let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+    let p = pr_tacarg_using_rule prgen (pl,l) in
+    if lev' > lev then surround p else p
   with Not_found ->
     str s ++ prlist prgen l ++ str " (* Generic printer *)"
 
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
+let pr_raw_extend prc prlc prtac = 
+  pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
+let pr_glob_extend prc prlc prtac =
+  pr_extend_gen (pr_glob_generic prc prlc prtac)
+let pr_extend prc prlc prtac =
+  pr_extend_gen (pr_generic prc prlc prtac)
+
+(**********************************************************************)
+(* The tactic printer                                                 *)
+
+let sep_v = fun _ -> str"," ++ spc()
+
+let strip_prod_binders_expr n ty =
+  let rec strip_ty acc n ty =
+    match ty with
+        Topconstr.CProdN(_,bll,a) ->
+          let nb =
+            List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
+          if nb >= n then (List.rev (bll@acc), a)
+          else strip_ty (bll@acc) (n-nb) a
+      | Topconstr.CArrow(_,a,b) ->
+          if n=1 then
+            (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
+          else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
+      | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let pr_ltac_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+
+let pr_arg pr x = spc () ++ pr x
+
+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) (Libnames.ConstRef sp)
+
+let pr_inductive env ind =
+  Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind)
+
+let pr_quantified_hypothesis = function
+  | AnonHyp n -> int n
+  | NamedHyp id -> pr_id id 
+
+let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
+
+let pr_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_constr prc = function
+  | None -> mt ()
+  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
+let pr_with_names = function
+  | IntroAnonymous -> mt ()
+  | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+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_with_names 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_with_names ipat
+
+let pr_by_tactic prt = function
+  | TacId [] -> mt ()
+  | tac -> spc() ++ str "by " ++ prt tac
+
+let pr_occs pp = function
+    [] -> pp
+  | nl -> hov 1 (pp ++ spc() ++ str"at " ++
+                 hov 0 (prlist_with_sep spc int nl))
+
+let pr_hyp_location pr_id = function
+  | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
+  | id, occs, InHypTypeOnly ->
+      spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
+  | id, occs, InHypValueOnly ->
+      spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+
+let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+
+let pr_simple_clause pr_id = function
+  | [] -> mt ()
+  | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+let pr_clauses pr_id = function
+    { onhyps=None; onconcl=true; concl_occs=nl } ->
+      pr_in (pr_occs (str " *") nl)
+  | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
+  | { onhyps=Some l; onconcl=true; concl_occs=nl } -> 
+      pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
+             ++ pr_occs (str" |- *") nl)
+  | { onhyps=Some l; onconcl=false } ->
+      pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
+
+let pr_clause_pattern pr_id = function
+  | (None, []) -> mt ()
+  | (glopt,l) ->
+      str " in" ++
+      prlist
+        (fun (id,nl) -> prlist (pr_arg int) nl 
+	  ++ spc () ++ pr_id id) l ++
+        pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
+
+let pr_induction_arg prc = function
+  | ElimOnConstr c -> prc c
+  | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+  | ElimOnAnonHyp n -> int n
+
+let pr_induction_kind = function
+  | SimpleInversion -> str "simple inversion"
+  | FullInversion -> str "inversion"
+  | FullInversionClear -> str "inversion_clear"
+
+let pr_lazy lz = if lz then str "lazy " else mt ()
+
+let pr_match_pattern pr_pat = function
+  | Term a -> pr_pat a
+  | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
+  | Subterm (Some id,a) ->
+      str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+
+let pr_match_hyps pr_pat = function
+  | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+
+let pr_match_rule m pr pr_pat = function
+  | Pat ([],mp,t) when m ->
+      pr_match_pattern pr_pat mp ++
+      spc () ++ str "=>" ++ brk (1,4) ++ pr t
+  | Pat (rl,mp,t) ->
+      prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
+      spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+      str "=>" ++ brk (1,4) ++ pr t
+  | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+
+let pr_funvar = function
+  | None -> spc () ++ str "_"
+  | Some id -> spc () ++ pr_id id
+
+let pr_let_clause k pr = function
+  | (id,None,t) ->
+      hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
+             pr (TacArg t))
+  | (id,Some c,t) ->
+      hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
+      pr c ++
+      str " :=" ++ brk (1,1) ++ pr (TacArg t))
+
+let pr_let_clauses pr = function
+  | hd::tl ->
+      hv 0
+        (pr_let_clause "let " pr hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
+  | [] -> anomaly "LetIn must declare at least one binding"
+
+let pr_rec_clause pr (id,(l,t)) =
+  hov 0
+    (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+
+let pr_rec_clauses pr l = 
+  prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
+
+let pr_seq_body pr tl =
+  hv 0 (str "[ " ++
+        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+        str " ]")
+
+let pr_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_coma prc l)
+
+let pr_autoarg_adding = function
+  | [] -> mt ()
+  | l ->
+      spc () ++ str "adding [" ++
+        hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
+
+let pr_autoarg_destructing = function
+  | true -> spc () ++ str "destructing"
+  | false -> mt ()
+
+let pr_autoarg_usingTDB = function
+  | true -> spc () ++ str "using tdb"
+  | false -> mt ()
+
+let rec pr_tacarg_using_rule pr_gen = function
+  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_then () = str ";"
 
-let pr_bindings = pr_bindings pr_constr pr_constr in
-let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in
-let pr_with_bindings = pr_with_bindings pr_constr pr_constr in
-let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in
-let pr_constrarg c = spc () ++ pr_constr c in
+let ltop = (5,E)
+let lseq = 5
+let ltactical = 3
+let lorelse = 2
+let llet = 1
+let lfun = 1
+let lcomplete = 1
+let labstract = 3
+let lmatch = 1
+let latom = 0
+let lcall = 1
+let leval = 1
+let ltatom = 1
+
+let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+
+open Closure
+
+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) =
+
+let pr_bindings env =
+  pr_bindings (pr_lconstr env) (pr_constr env) in
+let pr_ex_bindings env =
+  pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
+let pr_with_bindings env =
+  pr_with_bindings (pr_lconstr env) (pr_constr env) in
+let pr_eliminator env cb =
+  str "using" ++ pr_arg (pr_with_bindings env) cb in
+let pr_extend env =
+  pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) in
+let pr_red_expr env = 
+  pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) in
+
+let pr_constrarg env c = spc () ++ pr_constr env c in
+let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
 let pr_intarg n = spc () ++ int n in
 
+let pr_binder_fix env (nal,t) =
+(*  match t with
+  | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+  | _ ->*)
+    let s =
+      prlist_with_sep spc (pr_lname) nal ++ str ":" ++
+      pr_lconstr env t in
+    spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+let pr_fix_tac env (id,n,c) =
+  let rec set_nth_name avoid n = function
+      (nal,ty)::bll ->
+        if n <= List.length nal then
+          match list_chop (n-1) nal with
+              _, (_,Name id) :: _ -> id, (nal,ty)::bll
+            | bef, (loc,Anonymous) :: aft ->
+                let id = next_ident_away_from (id_of_string"y") avoid in
+                id, ((bef@(loc,Name id)::aft, ty)::bll)
+            | _ -> assert false
+        else
+          let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+          (id,(nal,ty)::bll')
+    | [] -> assert false in
+  let (bll,ty) = strip_prod_binders n c in
+  let names =
+    List.fold_left
+      (fun ln (nal,_) -> List.fold_left
+          (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+          ln nal)
+      [] bll in
+  let idarg,bll = set_nth_name names n bll in
+  let annot =
+    if List.length names = 1 then mt()
+    else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
+  hov 1 (str"(" ++ pr_id id ++ 
+        prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++
+        pr_lconstrarg env ty ++ str")") in
+(*  spc() ++
+  hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+    env c)
+*)
+let pr_cofix_tac env (id,c) =
+  hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
+
   (* Printing tactics as arguments *)
-let rec pr_atom0 = function
-  | TacIntroPattern [] -> str "Intros"
-  | TacIntroMove (None,None) -> str "Intro"
-  | TacAssumption -> str "Assumption"
-  | TacAnyConstructor None -> str "Constructor"
-  | TacTrivial (Some []) -> str "Trivial"
-  | TacAuto (None,Some []) -> str "Auto"
-  | TacAutoTDB None -> str "AutoTDB"
-  | TacDestructConcl -> str "DConcl"
-  | TacReflexivity -> str "Reflexivity"
-  | t -> str "(" ++ pr_atom1 t ++ str ")"
+let rec pr_atom0 env = function
+  | TacIntroPattern [] -> str "intros"
+  | TacIntroMove (None,None) -> str "intro"
+  | TacAssumption -> str "assumption"
+  | TacAnyConstructor None -> str "constructor"
+  | TacTrivial ([],Some []) -> str "trivial"
+  | TacAuto (None,[],Some []) -> str "auto"
+  | TacReflexivity -> str "reflexivity"
+  | t -> str "(" ++ pr_atom1 env t ++ str ")"
 
   (* Main tactic printer *)
-and pr_atom1 = function
-  | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac s l
-  | TacAlias (_,s,l,_) ->
-      pr_extend pr_constr pr_constr pr_tac s (List.map snd l)
+and pr_atom1 env = function
+  | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
+  | TacSuperAuto _ | TacExtend (_,
+    ("GTauto"|"GIntuition"|"TSimplif"|
+     "LinearIntuition"),_) ->
+      errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
+  | TacExtend (loc,s,l) ->
+      pr_with_comments loc (pr_extend env 1 s l)
+  | TacAlias (loc,s,l,_) ->
+      pr_with_comments loc (pr_extend env 1 s (List.map snd l))
 
   (* Basic tactics *)
-  | TacIntroPattern [] as t -> pr_atom0 t
+  | TacIntroPattern [] as t -> pr_atom0 env t
   | TacIntroPattern (_::_ as p) -> 
-      hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
+      hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
   | TacIntrosUntil h ->
-      hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h)
-  | TacIntroMove (None,None) as t -> pr_atom0 t
-  | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1
-  | TacIntroMove (ido1,Some (_,id2)) ->
+      hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
+  | TacIntroMove (None,None) as t -> pr_atom0 env t
+  | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
+  | TacIntroMove (ido1,Some id2) ->
       hov 1
-      (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
-  | TacAssumption as t -> pr_atom0 t
-  | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
-  | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
+      (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
+       pr_lident id2)
+  | TacAssumption as t -> pr_atom0 env t
+  | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
+  | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c)
+  | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
   | TacElim (cb,cbo) ->
-      hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ 
-        pr_opt pr_eliminator cbo)
-  | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c)
-  | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb)
-  | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
-  | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+      hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ 
+        pr_opt (pr_eliminator env) cbo)
+  | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c)
+  | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb)
+  | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
+  | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
-      hov 1 (str "Fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
-        hov 0 (str "with" ++ brk (1,1) ++
-          prlist_with_sep spc
-	    (fun (id,n,c) ->
-	      spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c)
-	  l))
-  | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido)
+      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
+             str"with " ++ prlist_with_sep spc (pr_fix_tac env) l)
+  | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
   | TacMutualCofix (id,l) ->
-      hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++
-        hov 0 (str "with" ++ brk (1,1) ++
-          prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
-	  l))
-  | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
-  | TacTrueCut (Anonymous,c) -> 
-      hov 1 (str "Assert" ++ pr_arg pr_constr c)
-  | TacTrueCut (Name id,c) -> 
-      hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
-  | TacForward (false,na,c) ->
-      hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
-  | TacForward (true,na,c) ->
-      hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
+      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
+             str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
+  | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
+  | TacAssert (Some tac,ipat,c) -> 
+      hov 1 (str "assert" ++ 
+             pr_assumption (pr_lconstr env) (pr_constr env) ipat c ++ 
+             pr_by_tactic (pr_tac_level env ltop) tac)
+  | TacAssert (None,ipat,c) -> 
+      hov 1 (str "pose proof" ++
+             pr_assertion (pr_lconstr env) (pr_constr env) ipat c)
   | TacGeneralize l ->
-      hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l)
+      hov 1 (str "generalize" ++ spc () ++
+             prlist_with_sep spc (pr_constr env) l)
   | TacGeneralizeDep c ->
-      hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
-      pr_constr c)
+      hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
+             pr_constrarg env c)
+  | TacLetTac (na,c,cl) when cl = nowhere ->
+      hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c)
   | TacLetTac (na,c,cl) ->
-      let pcl = match cl with
-          {onhyps=None;onconcl=true;concl_occs=[]} -> mt()
-        | _ -> pr_clauses pr_ident cl in
-      hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
-             pr_constr c ++ pcl)
-  | TacInstantiate (n,c,cls) ->
-      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
-	     pr_clauses pr_ident cls)
+      hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++
+             pr_clauses pr_ident cl)
+(*  | TacInstantiate (n,c,ConclLocation ()) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg env c ++ str ")" ))
+  | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg env c ++ str ")" ) 
+	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+*)
   (* Derived basic tactics *)
-  | TacSimpleInduction (h,_) ->
-      hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e,(ids,_)) ->
-      hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
-        pr_opt pr_eliminator e ++ pr_with_names ids)
+  | TacSimpleInduction h ->
+      hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewInduction (h,e,ids) ->
+      hov 1 (str "induction" ++ spc () ++
+	     prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
+             pr_opt (pr_eliminator env) e)
   | TacSimpleDestruct h ->
-      hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e,(ids,_)) ->
-      hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
-        pr_opt pr_eliminator e ++ pr_with_names ids)
+      hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
+  | TacNewDestruct (h,e,ids) ->
+      hov 1 (str "destruct" ++ spc () ++
+             prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ 
+	     pr_with_names ids ++
+             pr_opt (pr_eliminator env) e)
   | TacDoubleInduction (h1,h2) ->
       hov 1
-        (str "Double Induction" ++ 
+        (str "double induction" ++  
          pr_arg pr_quantified_hypothesis h1 ++
  	 pr_arg pr_quantified_hypothesis h2)
   | TacDecomposeAnd c ->
-      hov 1 (str "Decompose Record" ++ pr_arg pr_constr c)
+      hov 1 (str "decompose record" ++ pr_constrarg env c)
   | TacDecomposeOr c ->
-      hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c)
+      hov 1 (str "decompose sum" ++ pr_constrarg env c)
   | TacDecompose (l,c) ->
-      hov 1 (str "Decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
-	  ++ str "]" ++ pr_arg pr_constr c))
+      hov 1 (str "decompose" ++ spc () ++
+        hov 0 (str "[" ++ prlist_with_sep spc (pr_ind env) l
+	  ++ str "]" ++ pr_constrarg env c))
   | TacSpecialize (n,c) ->
-      hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
+      hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ 
+             pr_with_bindings env c)
   | TacLApply c -> 
-      hov 1 (str "LApply" ++ pr_constr c)
+      hov 1 (str "lapply" ++ pr_constrarg env c)
 
   (* Automation tactics *)
-  | TacTrivial (Some []) as x -> pr_atom0 x
-  | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
-  | TacAuto (None,Some []) as x -> pr_atom0 x
-  | TacAuto (n,db) ->
-      hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
-  | TacAutoTDB None as x -> pr_atom0 x
-  | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
-  | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
-  | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id)
-  | TacDestructConcl as x -> pr_atom0 x
-  | TacSuperAuto (n,l,b1,b2) ->
-      hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
-             pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
+  | TacTrivial ([],Some []) as x -> pr_atom0 env x
+  | TacTrivial (lems,db) ->
+      hov 0 (str "trivial" ++ 
+             pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
+  | TacAuto (None,[],Some []) as x -> pr_atom0 env x
+  | TacAuto (n,lems,db) ->
+      hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ 
+             pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
   | TacDAuto (n,p) ->
-      hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ 
-      pr_opt int p)
+      hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
 
   (* Context management *)
-  | TacClear l ->
-      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+  | 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)
+      hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
       (* Rem: only b = true is available for users *)
       assert b;
       hov 1
-        (str "Move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
+        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
 	 str "after" ++ brk (1,1) ++ pr_ident id2)
   | TacRename (id1,id2) ->
       hov 1
-        (str "Rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
+        (str "rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
 	 str "into" ++ brk (1,1) ++ pr_ident id2)
 
   (* Constructors *)
-  | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
-  | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
-  | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l)
+  | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l)
+  | TacRight l -> hov 1 (str "right" ++ pr_bindings env l)
+  | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l)
+  | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l)
   | TacAnyConstructor (Some t) ->
-      hov 1 (str "Constructor" ++ pr_arg pr_tac0 t)
-  | TacAnyConstructor None as t -> pr_atom0 t
+      hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t)
+  | TacAnyConstructor None as t -> pr_atom0 env t
   | TacConstructor (n,l) ->
-      hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
+      hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l)
 
   (* Conversion *)  
   | TacReduce (r,h) ->
-      hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clauses pr_ident h)
-  | TacChange (occl,c,h) ->
-      hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ 
-        brk (1,1) ++ pr_constr c ++ pr_clauses pr_ident h)
+      hov 1 (pr_red_expr env r ++
+             pr_clauses pr_ident h)
+  | TacChange (occ,c,h) ->
+      hov 1 (str "change" ++ brk (1,1) ++
+      (match occ with
+          None -> mt()
+        | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
+        | Some(ocl,c1) ->
+            hov 1 (pr_constr env c1 ++ spc() ++
+	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "with ") ++
+      pr_constr env c ++ pr_clauses pr_ident h)
 
   (* Equivalence relations *)
-  | TacReflexivity as x -> pr_atom0 x
-  | TacSymmetry cls -> str "Symmetry " ++ pr_clauses pr_ident cls
-  | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
+  | TacReflexivity as x -> pr_atom0 env x
+  | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
+  | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c
 
   (* Equality and inversion *)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      hov 1 (str "Dependent " ++ pr_induction_kind k ++ 
+      hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_names ids ++ pr_with_constr pr_constr c)
+      pr_with_names ids ++ pr_with_constr (pr_constr env) c)
   | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
       hov 1 (pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
       pr_with_names ids ++ pr_simple_clause pr_ident cl)
   | TacInversion (InversionUsing (c,cl),hyp) ->
-      hov 1 (str "Inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
-      str "using" ++ spc () ++ pr_constr c ++ 
+      hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
+      spc () ++ str "using" ++ spc () ++ pr_constr env c ++ 
       pr_simple_clause pr_ident cl)
 
-and pr_tactic_seq_body tl = 
-  hv 0 (str "[ " ++
-        prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
-
-  (* Strictly closed atomic tactic expressions *)
-and pr0 = function
-  | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
-  | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
-  | TacId "" -> str "Idtac" 
-  | TacFail (ArgArg 0,"") -> str "Fail"
-  | TacAtom (_,t) -> pr_atom0 t
-  | TacArg c -> pr_tacarg c
-  | t -> str "(" ++ prtac t ++ str ")"
-
-  (* Semi-closed atomic tactic expressions *)
-and pr1 = function
-  | TacAtom (_,t) -> pr_atom1 t
-  | TacId s -> str "Idtac \"" ++ str s ++ str "\""	
-  | TacFail (ArgArg 0,s) -> str "Fail \"" ++ str s ++ str "\""
-  | TacFail (n,"") -> str "Fail " ++ pr_or_var int n
-  | TacFail (n,s) -> str "Fail " ++ pr_or_var int n ++ str " \"" ++ str s ++ str "\""
-  | t -> pr0 t
-
-  (* Orelse tactic expressions (printed as if parsed associating on the right
-     though the semantics is purely associative) *)
-and pr2 = function
-  | TacOrelse (t1,t2) ->
-      hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2)
-  | t -> pr1 t
-
-  (* Non closed prefix tactic expressions *)
-and pr3 = function
-  | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t)
-  | TacDo (n,t) -> hov 1 (str "Do " ++ pr_or_var int n ++ spc () ++ pr3 t)
-  | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
-  | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
-  | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
-  | t -> pr2 t
-
-and pr4 = function
-  | t -> pr3 t
-
-  (* THEN and THENS tactic expressions (printed as if parsed
-     associating on the left though the semantics is purely associative) *)
-and pr5 = function
-  | TacThens (t,tl) -> 
-      hov 1 (pr5 t ++ str ";" ++ spc () ++ pr_tactic_seq_body tl)
-  | TacThen (t1,t2) ->
-      hov 1 (pr5 t1 ++ str ";" ++ spc () ++ pr4 t2)
-  | t -> pr4 t
-
-  (* Ltac tactic expressions *)
-and pr6 = function
-  |(TacAtom _
-  | TacThen _
-  | TacThens _
-  | TacFirst _
-  | TacSolve _
-  | TacTry _
-  | TacOrelse _
-  | TacDo _
-  | TacRepeat _
-  | TacProgress _
-  | TacId _
-  | TacFail _
-  | TacInfo _) as t -> pr5 t
-
-  | TacAbstract (t,None) -> str "Abstract " ++ pr6 t
+in
+
+let rec pr_tac env inherited tac =
+  let (strm,prec) = match tac with
+  | TacAbstract (t,None) ->
+      str "abstract " ++ pr_tac env (labstract,L) t, labstract
   | TacAbstract (t,Some s) -> 
       hov 0
-       (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s)
+       (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++
+        str "using " ++ pr_id s),
+      labstract
   | TacLetRecIn (l,t) -> 
       hv 0
-        (str "Rec " ++ pr_rec_clauses prtac l ++
-        spc () ++ str "In" ++ fnl () ++ prtac t)
+        (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++
+         fnl () ++ pr_tac env (llet,E) t),
+      llet
   | TacLetIn (llc,u) ->
       v 0
-       (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
-  | TacMatch (t,lrul) ->
-      hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc()
-        ++ str "With"
+       (hv 0 (pr_let_clauses (pr_tac env ltop) llc
+       ++ str " in") ++
+       fnl () ++ pr_tac env (llet,E) u),
+      llet
+  | TacMatch (lz,t,lrul) ->
+      hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with"
         ++ prlist
-	  (fun r -> fnl () ++ str "|" ++ spc () ++
-            pr_match_rule true pr_pat prtac r)
-	lrul)
-  | TacMatchContext (lr,lrul) ->
-      hov 0 (
-	str (if lr then "Match Reverse Context With" else "Match Context With")
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule true (pr_tac env ltop) pr_pat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
+  | TacMatchContext (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 "|" ++ spc () ++
-            pr_match_rule false pr_pat prtac r)
-	lrul)
+	  (fun r -> fnl () ++ str "| " ++
+            pr_match_rule false (pr_tac env ltop) pr_pat r)
+	lrul
+        ++ fnl() ++ str "end"),
+      lmatch
   | TacFun (lvar,body) ->
-      hov 0 (str "Fun" ++
-        prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body)
-
-  | TacArg c -> pr_tacarg c
-
-and pr_tacarg0 = function
-  | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
-  | MetaIdArg (_,s) -> str ("$" ^ s)
-  | IntroPattern ipat -> pr_intro_pattern ipat
+(*      let env = List.fold_right (option_fold_right Idset.add) lvar env in*)
+      hov 2 (str "fun" ++
+        prlist pr_funvar lvar ++ str " =>" ++ spc () ++
+        pr_tac env (lfun,E) body),
+      lfun
+  | TacThens (t,tl) -> 
+      hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++
+             pr_seq_body (pr_tac env ltop) tl),
+      lseq
+  | TacThen (t1,t2) ->
+      hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++
+             pr_tac env (lseq,L) t2),
+      lseq
+  | TacTry t ->
+      hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacDo (n,t) ->
+      hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ 
+             pr_tac env (ltactical,E) t),
+      ltactical
+  | TacRepeat t ->
+      hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacProgress t ->
+      hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacInfo t ->
+      hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t),
+      ltactical
+  | TacOrelse (t1,t2) ->
+      hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+             pr_tac env (lorelse,E) t2),
+      lorelse
+  | TacFail (n,l) -> 
+      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 env ltop) tl, llet
+  | TacSolve tl ->
+      str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+  | TacComplete t ->
+      str "complete" ++ spc () ++ pr_tac env (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 env (level_of inherited) s (List.map snd l)),
+      latom
+  | TacAtom (loc,t) ->
+      pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
+  | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom
+  | TacArg(ConstrMayEval (ConstrTerm c)) ->
+      str "constr:" ++ pr_constr env c, latom
+  | TacArg(ConstrMayEval c) ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
+  | TacArg(Integer n) -> int n, latom
+  | TacArg(TacCall(loc,f,l)) ->
+      pr_with_comments loc
+        (hov 1 (pr_ref f ++ spc () ++
+         prlist_with_sep spc (pr_tacarg env) l)),
+      lcall
+  | TacArg a -> pr_tacarg env a, latom
+  in
+  if prec_less prec inherited then strm
+  else str"(" ++ strm ++ str")"
+
+and pr_tacarg env = function
+  | TacDynamic (loc,t) ->
+      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
+  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
-  | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
-  | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c
-  | Integer n -> int n
-  | TacFreshId sopt -> str "FreshId" ++ pr_opt qstring sopt
-  | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
-
-and pr_tacarg1 = function
-  | TacCall (_,f,l) ->
-      hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
-  | Tacexp t -> pr_tac t
-  | t -> pr_tacarg0 t
-
-and pr_tacarg x = pr_tacarg1 x
-
-and prtac x = pr6 x
-
-in (prtac,pr0,pr_match_rule false pr_pat pr_tac)
-
-let pr_raw_extend prc prlc prtac = 
-  pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference)
-let pr_glob_extend prc prlc prtac =
-  pr_extend_gen (pr_glob_generic prc prlc prtac)
-let pr_extend prc prlc prtac =
-  pr_extend_gen (pr_generic prc prlc prtac)
+  | ConstrMayEval c ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
+  | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
+  | TacExternal (_,com,req,la) ->
+      str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ 
+      spc() ++ prlist_with_sep spc (pr_tacarg env) la
+  | (TacCall _|Tacexp _|Integer _) as a ->
+      str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
+
+in (pr_tac, pr_match_rule)
+
+let strip_prod_binders_rawterm n (ty,_) =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, (ty,None)) else
+      match ty with
+          Rawterm.RProd(loc,na,a,b) ->
+            strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let strip_prod_binders_constr n ty =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, ty) else
+      match Term.kind_of_term ty with
+          Term.Prod(na,a,b) ->
+            strip_ty (([dummy_loc,na],a)::acc) (n-1) b
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let drop_env f _env = f
+
+let rec raw_printers =
+    (pr_raw_tactic_level, 
+     drop_env pr_constr_expr,
+     drop_env pr_lconstr_expr,
+     pr_pattern_expr,
+     drop_env pr_reference,
+     drop_env 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
+
+and pr_raw_match_rule env t =
+  snd (make_pr_tac raw_printers) env t
 
 let pr_and_constr_expr pr (c,_) = pr c
 
 let rec glob_printers =
-    (pr_glob_tactic, 
-     pr_glob_tactic0,
-     pr_and_constr_expr Printer.pr_rawterm,
-     Printer.pr_pattern,
-     pr_or_var (pr_and_short_name pr_evaluable_reference),
-     pr_or_var pr_inductive,
-     pr_or_var (pr_located pr_ltac_constant),
-     pr_located pr_id,
-     pr_glob_extend)
-
-and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t
-
-and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t
-
-and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t
-
-let (pr_tactic,_,_) =
+    (pr_glob_tactic_level, 
+     (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
+     (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
+     (fun c -> pr_constr_pattern_env (Global.env()) c),
+     (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_rawterm)
+
+and pr_glob_tactic_level env n (t:glob_tactic_expr) =
+  fst (make_pr_tac glob_printers) env n t
+
+and pr_glob_match_rule env t =
+  snd (make_pr_tac glob_printers) env t
+
+let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) =
   make_pr_tac
-    (pr_glob_tactic,
-     pr_glob_tactic0,
-     Printer.prterm,
-     Printer.pr_pattern,
-     pr_evaluable_reference,
+    (pr_glob_tactic_level,
+     pr_constr_env,
+     pr_lconstr_env,
+     pr_constr_pattern,
+     pr_evaluable_reference_env,
      pr_inductive,
      pr_ltac_constant,
      pr_id,
-     pr_extend)
+     pr_extend,
+     strip_prod_binders_constr)
+
+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())) pr_constr_pattern rl)