Partial disentangling of Ltac codebase.

24 files changed, 138 insertions, 213 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 39e4b1cdb1..7710033dba 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -174,7 +174,6 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Proof_type
 Goal
 Miscprint
 Logic
@@ -188,7 +187,6 @@ Proofview
 Proof
 Proof_global
 Pfedit
-Tactic_debug
 Decl_mode
 Ppconstr
 Entry
@@ -200,6 +198,7 @@ Egramml
 Egramcoq
 Tacsubst
 Tacenv
+Tactic_debug
 Trie
 Dn
 Btermdn
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index fc7cb392bf..296d32dc04 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -29,35 +29,22 @@ CStack
 Util
 Ppstyle
 Errors
-Bigint
 Predicate
 Segmenttree
 Unicodetable
 Unicode
 Genarg
 
-Evar
 Names
 
-Libnames
-
-Redops
-Miscops
-Locusops
-
 Stdarg
 Constrarg
-Constrexpr_ops
 
 Tok
 Compat
 Lexer
 Entry
 Pcoq
-G_prim
-G_tactic
-G_ltac
-G_constr
 
 Q_util
 Egramml
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index f2a567c00d..b1dc174d4b 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -394,3 +394,15 @@ type tactic_arg =
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+  | LtacMLCall of glob_tactic_expr
+  | LtacNotationCall of KerName.t
+  | LtacNameCall of ltac_constant
+  | LtacAtomCall of glob_atomic_tactic_expr
+  | LtacVarCall of Id.t * glob_tactic_expr
+  | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+
+type ltac_trace = (Loc.t * ltac_call_kind) list
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 7273b92b9a..5501ca7c7f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -69,7 +69,6 @@ type printable =
   | PrintHint of reference or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string
-  | PrintRewriteHintDbName of string
   | PrintHintDb
   | PrintScopes
   | PrintScope of string
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b5e9f9e067..49baeb5560 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -951,7 +951,6 @@ GEXTEND Gram
       | IDENT "Hint"; qid = smart_global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
-      | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index fdc1288aec..7d5e7772c3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1415,17 +1415,6 @@ let () =
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_tactic printer printer printer
 
-let _ = Hook.set Tactic_debug.tactic_printer
-  (fun x -> pr_glob_tactic (Global.env()) x)
-
-let _ = Hook.set Tactic_debug.match_pattern_printer
-  (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
-
-let _ = Hook.set Tactic_debug.match_rule_printer
-  (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env()))
-      (fun (_,p) -> pr_constr_pattern p) rl)
-
 module Richpp = struct
 
   include Make (Ppconstr.Richpp) (struct
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c5ec6bb092..b98b6c67e7 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -67,4 +67,9 @@ module type Pp = sig
     ('constr -> std_ppcmds) ->
     ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
 
+  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('b, 'a) match_rule -> std_ppcmds
+
 end
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ffec926a84..a101540aba 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -486,8 +486,6 @@ module Make
         keyword "Print Hint *"
       | PrintHintDbName s ->
         keyword "Print HintDb" ++ spc () ++ str s
-      | PrintRewriteHintDbName s ->
-        keyword "Print Rewrite HintDb" ++ spc() ++ str s
       | PrintUniverses (b, fopt) ->
         let cmd =
           if b then "Print Sorted Universes"
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
deleted file mode 100644
index dd2c7b253d..0000000000
--- a/proofs/proof_type.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i*)
-open Evd
-open Names
-open Term
-open Tacexpr
-open Glob_term
-open Nametab
-open Misctypes
-(*i*)
-
-(* This module defines the structure of proof tree and the tactic type. So, it
-   is used by Proof_tree and Refiner *)
-
-(** Types of goals, tactics, rules ... *)
-
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma 
-
-type prim_rule =
-  | Cut of bool * bool * Id.t * types
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
-  | Cofix of Id.t * (Id.t * constr) list * int
-  | Refine of constr
-  | Thin of Id.t list
-  | Move of Id.t * Id.t move_location
-
-(** Nowadays, the only rules we'll consider are the primitive rules *)
-
-type rule = prim_rule
-
-(** Ltac traces *)
-
-type ltac_call_kind =
-  | LtacMLCall of glob_tactic_expr
-  | LtacNotationCall of KerName.t
-  | LtacNameCall of ltac_constant
-  | LtacAtomCall of glob_atomic_tactic_expr
-  | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index aa05f58ab6..b4c9dae2a3 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -57,19 +57,3 @@ type rule = prim_rule
 type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma
-
-(** Ltac traces *)
-
-(** TODO: Move those definitions somewhere sensible *)
-
-type ltac_call_kind =
-  | LtacMLCall of glob_tactic_expr
-  | LtacNotationCall of KerName.t
-  | LtacNameCall of ltac_constant
-  | LtacAtomCall of glob_atomic_tactic_expr
-  | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-val ltac_trace_info : ltac_trace Exninfo.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 1bd701cb9b..08556d62ec 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,7 +2,6 @@ Miscprint
 Goal
 Evar_refiner
 Proof_using
-Proof_type
 Proof_errors
 Logic
 Proofview
@@ -12,6 +11,5 @@ Redexpr
 Refiner
 Tacmach
 Pfedit
-Tactic_debug
 Clenv
 Clenvtac
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 55463afd01..588709873e 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -99,8 +99,6 @@ end
 module Ftac = Monad.Make(Self)
 module List = Ftac.List
 
-let debug_prompt = Tactic_debug.debug_prompt
-
 module Notations =
 struct
   let (>>=) = bind
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index fd05a44698..19041f1698 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -70,11 +70,6 @@ val (<*>) : unit t -> 'a t -> 'a t
 
 module List : Monad.ListS with type 'a t := 'a t
 
-(** {5 Debug} *)
-
-val debug_prompt :
-  int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t
-
 (** {5 Notations} *)
 
 module Notations :
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 72cfb01a57..6b6dc7b21a 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -261,3 +261,7 @@ TACTIC EXTEND setoid_transitivity
   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
 | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
 END
+
+VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
+  [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
+END
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 0d73cc27aa..73f11d0be0 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,5 +1,6 @@
 Extraargs
 Coretactics
+Autorewrite
 Extratactics
 Eauto
 G_auto
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf5f9ddc86..32f7c3c61c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,6 +44,8 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+let ltac_trace_info = Tactic_debug.ltac_trace_info
+
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
   match Val.eq t (val_tag wit) with
@@ -1200,7 +1202,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
           let ist = { ist with extra = TacStore.set ist.extra f_debug v } in
           value_interp ist >>= fun v -> return (name_vfun appl v)
         in
-	Ftactic.debug_prompt lev tac eval
+	Tactic_debug.debug_prompt lev tac eval
   | _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
       
 
@@ -2199,3 +2201,16 @@ let lift_constr_tac_to_ml_tac vars tac =
     tac args ist
   end } in
   tac
+
+let vernac_debug b =
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac debug";
+      optkey   = ["Ltac";"Debug"];
+      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
+      optwrite = vernac_debug }
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c5da3494cb..31327873e9 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -14,6 +14,8 @@ open Genarg
 open Redexpr
 open Misctypes
 
+val ltac_trace_info : ltac_trace Exninfo.t
+
 module Value :
 sig
   type t = Val.t
diff --git a/proofs/tactic_debug.ml b/tactics/tactic_debug.ml
index d33278ff8d..e991eb86dc 100644
--- a/proofs/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -14,10 +14,15 @@ open Termops
 open Nameops
 open Proofview.Notations
 
-let (prtac, tactic_printer) = Hook.make ()
-let (prmatchpatt, match_pattern_printer) = Hook.make ()
-let (prmatchrl, match_rule_printer) = Hook.make ()
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
+let prtac x =
+  Pptactic.pr_glob_tactic (Global.env()) x
+let prmatchpatt env sigma hyp =
+  Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
+let prmatchrl rl =
+  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+    (fun (_,p) -> Printer.pr_constr_pattern p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -67,7 +72,7 @@ let help () =
 let goal_com tac =
   Proofview.tclTHEN
     db_pr_goal
-    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)))
+    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ prtac tac)))
 
 (* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
    expressions. It avoids parametrizing everything over a
@@ -228,7 +233,7 @@ let db_pattern_rule debug num r =
   if db then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
-      str "|" ++ spc () ++ Hook.get prmatchrl r)
+      str "|" ++ spc () ++ prmatchrl r)
   end
   else return ()
 
@@ -270,7 +275,7 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   if db then
     msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
                 str " cannot match: " ++
-           Hook.get prmatchpatt env sigma hyp)
+           prmatchpatt env sigma hyp)
   else return ()
 
 (* Prints a matching failure message for a rule *)
@@ -317,3 +322,79 @@ let db_breakpoint debug s =
       breakpoint:=None
   | _ ->
       return ()
+
+(** Extrating traces *)
+
+let is_defined_ltac trace =
+  let rec aux = function
+  | (_, Tacexpr.LtacNameCall f) :: tail ->
+      not (Tacenv.is_ltac_for_ml_tactic f)
+  | (_, Tacexpr.LtacAtomCall _) :: tail ->
+      false
+  | _ :: tail -> aux tail
+  | [] -> false in
+  aux (List.rev trace)
+
+let explain_ltac_call_trace last trace loc =
+  let calls = last :: List.rev_map snd trace in
+  let pr_call ck = match ck with
+  | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+  | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Tacexpr.LtacMLCall t ->
+      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+  | Tacexpr.LtacVarCall (id,t) ->
+      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+  | Tacexpr.LtacAtomCall te ->
+      quote (Pptactic.pr_glob_tactic (Global.env())
+              (Tacexpr.TacAtom (Loc.ghost,te)))
+  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+        (if not (Id.Map.is_empty vars) then
+          strbrk " (with " ++
+            prlist_with_sep pr_comma
+            (fun (id,c) ->
+                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+            (List.rev (Id.Map.bindings vars)) ++ str ")"
+        else mt())
+  in
+  match calls with
+  | [] -> mt ()
+  | _ ->
+    let kind_of_last_call = match List.last calls with
+    | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
+    | _ -> ", last call failed."
+    in
+    hov 0 (str "In nested Ltac calls to " ++
+           pr_enum pr_call calls ++ strbrk kind_of_last_call)
+
+let skip_extensions trace =
+  let rec aux = function
+  | (_,Tacexpr.LtacNameCall f as tac) :: _ 
+      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
+  | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
+      :: _ -> [tac]
+  | t :: tail -> t :: aux tail
+  | [] -> [] in
+  List.rev (aux (List.rev trace))
+
+let extract_ltac_trace trace eloc =
+  let trace = skip_extensions trace in
+  let (loc,c),tail = List.sep_last trace in
+  if is_defined_ltac trace then
+    (* We entered a user-defined tactic,
+       we display the trace with location of the call *)
+    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
+    Some msg, loc
+  else
+    (* We entered a primitive tactic, we don't display trace but
+       report on the finest location *)
+    let best_loc =
+      if not (Loc.is_ghost eloc) then eloc else
+        (* trace is with innermost call coming first *)
+        let rec aux = function
+        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
+        | _::tail -> aux tail
+        | [] -> Loc.ghost in
+        aux trace in
+    None, best_loc
diff --git a/proofs/tactic_debug.mli b/tactics/tactic_debug.mli
index 215c5b29b5..523398e75a 100644
--- a/proofs/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -13,16 +13,14 @@ open Tacexpr
 open Term
 open Evd
 
+(** TODO: Move those definitions somewhere sensible *)
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
 (** This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
    complete panel of commands dedicated to a proof assistant framework *)
 
-val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
-val match_pattern_printer :
-  (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
-val match_rule_printer :
-  ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
-
 (** Debug information *)
 type debug_info =
   | DebugOn of int
@@ -77,3 +75,6 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
   Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
+
+val extract_ltac_trace :
+  Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 2c5edc20ed..fd7fab0c58 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -21,8 +21,8 @@ Hints
 Auto
 Tacintern
 Tactic_matching
+Tactic_debug
 Tacinterp
 Evar_tactics
 Term_dnet
-Autorewrite
 Tactic_option
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 600683d359..0b8edd91c1 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -120,13 +120,13 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
       let err = Errors.make_anomaly msg in
       Util.iraise (err, info)
   in
-  let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
+  let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
   | None -> e
   | Some trace ->
     let (e, info) = e in
-    match Himsg.extract_ltac_trace trace loc with
+    match Tactic_debug.extract_ltac_trace trace loc with
     | None, loc -> (e, Loc.add_loc info loc)
     | Some msg, loc ->
       (EvaluatedError (msg, Some e), Loc.add_loc info loc)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index de7ec61c81..4ee1537c20 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1244,77 +1244,3 @@ let explain_reduction_tactic_error = function
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' Evd.empty e
-
-let is_defined_ltac trace =
-  let rec aux = function
-  | (_, Proof_type.LtacNameCall f) :: tail ->
-      not (Tacenv.is_ltac_for_ml_tactic f)
-  | (_, Proof_type.LtacAtomCall _) :: tail ->
-      false
-  | _ :: tail -> aux tail
-  | [] -> false in
-  aux (List.rev trace)
-
-let explain_ltac_call_trace last trace loc =
-  let calls = last :: List.rev_map snd trace in
-  let pr_call ck = match ck with
-  | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
-  | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
-  | Proof_type.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
-  | Proof_type.LtacVarCall (id,t) ->
-      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-  | Proof_type.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (Loc.ghost,te)))
-  | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
-      quote (pr_glob_constr_env (Global.env()) c) ++
-        (if not (Id.Map.is_empty vars) then
-          strbrk " (with " ++
-            prlist_with_sep pr_comma
-            (fun (id,c) ->
-                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-            (List.rev (Id.Map.bindings vars)) ++ str ")"
-        else mt())
-  in
-  match calls with
-  | [] -> mt ()
-  | _ ->
-    let kind_of_last_call = match List.last calls with
-    | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
-    | _ -> ", last call failed."
-    in
-    hov 0 (str "In nested Ltac calls to " ++
-           pr_enum pr_call calls ++ strbrk kind_of_last_call)
-
-let skip_extensions trace =
-  let rec aux = function
-  | (_,Proof_type.LtacNameCall f as tac) :: _ 
-      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac)
-      :: _ -> [tac]
-  | t :: tail -> t :: aux tail
-  | [] -> [] in
-  List.rev (aux (List.rev trace))
-
-let extract_ltac_trace trace eloc =
-  let trace = skip_extensions trace in
-  let (loc,c),tail = List.sep_last trace in
-  if is_defined_ltac trace then
-    (* We entered a user-defined tactic,
-       we display the trace with location of the call *)
-    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
-    Some msg, loc
-  else
-    (* We entered a primitive tactic, we don't display trace but
-       report on the finest location *)
-    let best_loc =
-      if not (Loc.is_ghost eloc) then eloc else
-        (* trace is with innermost call coming first *)
-        let rec aux = function
-        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
-        | _::tail -> aux tail
-        | [] -> Loc.ghost in
-        aux trace in
-    None, best_loc
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3ef98380b5..ced54fd279 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -36,9 +36,6 @@ val explain_pattern_matching_error :
 val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
-val extract_ltac_trace :
-  Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
-
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
 
 val explain_module_internalization_error :
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 38832b422f..c63dac3026 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1433,18 +1433,6 @@ let _ =
       optread  = Flags.get_dump_bytecode;
       optwrite = Flags.set_dump_bytecode }
 
-let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-
-let _ =
-  declare_bool_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Ltac debug";
-      optkey   = ["Ltac";"Debug"];
-      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
-      optwrite = vernac_debug }
-
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -1641,7 +1629,6 @@ let vernac_print = function
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
   | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
-  | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s)
   | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
   | PrintScopes ->
       msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))