Quick-and-dirty backtrace mechanism for the interpreter.

10 files changed, 335 insertions, 285 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 793cb3e535..17fa7c28f4 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -14,7 +14,6 @@ open Genarg
 open Tac2env
 open Tac2dyn
 open Tac2expr
-open Tac2interp
 open Tac2entries.Pltac
 open Proofview.Notations
 
@@ -90,22 +89,26 @@ let of_result f = function
 
 (** Stdlib exceptions *)
 
-let err_notfocussed =
-  LtacError (coq_core "Not_focussed", [||])
+let err_notfocussed bt =
+  Tac2interp.LtacError (coq_core "Not_focussed", [||], bt)
 
-let err_outofbounds =
-  LtacError (coq_core "Out_of_bounds", [||])
+let err_outofbounds bt =
+  Tac2interp.LtacError (coq_core "Out_of_bounds", [||], bt)
 
-let err_notfound =
-  LtacError (coq_core "Not_found", [||])
+let err_notfound bt =
+  Tac2interp.LtacError (coq_core "Not_found", [||], bt)
 
-let err_matchfailure =
-  LtacError (coq_core "Match_failure", [||])
+let err_matchfailure bt =
+  Tac2interp.LtacError (coq_core "Match_failure", [||], bt)
 
 (** Helper functions *)
 
-let thaw f = interp_app f [v_unit]
-let throw e = Proofview.tclLIFT (Proofview.NonLogical.raise e)
+let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+let throw bt e = Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
+
+let set_bt bt e = match e with
+| Tac2interp.LtacError (kn, args, _) -> Tac2interp.LtacError (kn, args, bt)
+| e -> e
 
 let return x = Proofview.tclUNIT x
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -116,13 +119,13 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
-let assert_focussed =
+let assert_focussed bt =
   Proofview.Goal.goals >>= fun gls ->
   match gls with
   | [_] -> Proofview.tclUNIT ()
-  | [] | _ :: _ :: _ -> throw err_notfocussed
+  | [] | _ :: _ :: _ -> throw bt err_notfocussed
 
-let pf_apply f =
+let pf_apply bt f =
   Proofview.Goal.goals >>= function
   | [] ->
     Proofview.tclENV >>= fun env ->
@@ -132,61 +135,61 @@ let pf_apply f =
     gl >>= fun gl ->
     f (Proofview.Goal.env gl) (Tacmach.New.project gl)
   | _ :: _ :: _ ->
-    throw err_notfocussed
+    throw bt err_notfocussed
 
 (** Primitives *)
 
-let define0 name f = Tac2env.define_primitive (pname name) begin function
-| [_] -> f
+let define0 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [_] -> f bt
 | _ -> assert false
 end
 
-let define1 name f = Tac2env.define_primitive (pname name) begin function
-| [x] -> f x
+let define1 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x] -> f bt x
 | _ -> assert false
 end
 
-let define2 name f = Tac2env.define_primitive (pname name) begin function
-| [x; y] -> f x y
+let define2 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x; y] -> f bt x y
 | _ -> assert false
 end
 
-let define3 name f = Tac2env.define_primitive (pname name) begin function
-| [x; y; z] -> f x y z
+let define3 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x; y; z] -> f bt x y z
 | _ -> assert false
 end
 
 (** Printing *)
 
-let () = define1 "print" begin fun pp ->
+let () = define1 "print" begin fun _ pp ->
   wrap_unit (fun () -> Feedback.msg_notice (Value.to_pp pp))
 end
 
-let () = define1 "message_of_int" begin fun n ->
+let () = define1 "message_of_int" begin fun _ n ->
   let n = Value.to_int n in
   return (Value.of_pp (int n))
 end
 
-let () = define1 "message_of_string" begin fun s ->
+let () = define1 "message_of_string" begin fun _ s ->
   let s = Value.to_string s in
   return (Value.of_pp (str (Bytes.to_string s)))
 end
 
-let () = define1 "message_of_constr" begin fun c ->
-  pf_apply begin fun env sigma ->
+let () = define1 "message_of_constr" begin fun bt c ->
+  pf_apply bt begin fun env sigma ->
     let c = Value.to_constr c in
     let pp = Printer.pr_econstr_env env sigma c in
     return (Value.of_pp pp)
   end
 end
 
-let () = define1 "message_of_ident" begin fun c ->
+let () = define1 "message_of_ident" begin fun _ c ->
   let c = Value.to_ident c in
   let pp = Id.print c in
   return (Value.of_pp pp)
 end
 
-let () = define2 "message_concat" begin fun m1 m2 ->
+let () = define2 "message_concat" begin fun _ m1 m2 ->
   let m1 = Value.to_pp m1 in
   let m2 = Value.to_pp m2 in
   return (Value.of_pp (Pp.app m1 m2))
@@ -194,45 +197,45 @@ end
 
 (** Array *)
 
-let () = define2 "array_make" begin fun n x ->
+let () = define2 "array_make" begin fun bt n x ->
   let n = Value.to_int n in
-  if n < 0 || n > Sys.max_array_length then throw err_outofbounds
+  if n < 0 || n > Sys.max_array_length then throw bt err_outofbounds
   else wrap (fun () -> ValBlk (0, Array.make n x))
 end
 
-let () = define1 "array_length" begin fun v ->
+let () = define1 "array_length" begin fun _ v ->
   let v = to_block v in
   return (ValInt (Array.length v))
 end
 
-let () = define3 "array_set" begin fun v n x ->
+let () = define3 "array_set" begin fun bt v n x ->
   let v = to_block v in
   let n = Value.to_int n in
-  if n < 0 || n >= Array.length v then throw err_outofbounds
+  if n < 0 || n >= Array.length v then throw bt err_outofbounds
   else wrap_unit (fun () -> v.(n) <- x)
 end
 
-let () = define2 "array_get" begin fun v n ->
+let () = define2 "array_get" begin fun bt v n ->
   let v = to_block v in
   let n = Value.to_int n in
-  if n < 0 || n >= Array.length v then throw err_outofbounds
+  if n < 0 || n >= Array.length v then throw bt err_outofbounds
   else wrap (fun () -> v.(n))
 end
 
 (** Ident *)
 
-let () = define2 "ident_equal" begin fun id1 id2 ->
+let () = define2 "ident_equal" begin fun _ id1 id2 ->
   let id1 = Value.to_ident id1 in
   let id2 = Value.to_ident id2 in
   return (Value.of_bool (Id.equal id1 id2))
 end
 
-let () = define1 "ident_to_string" begin fun id ->
+let () = define1 "ident_to_string" begin fun _ id ->
   let id = Value.to_ident id in
   return (Value.of_string (Id.to_string id))
 end
 
-let () = define1 "ident_of_string" begin fun s ->
+let () = define1 "ident_of_string" begin fun _ s ->
   let s = Value.to_string s in
   let id = try Some (Id.of_string s) with _ -> None in
   return (Value.of_option Value.of_ident id)
@@ -240,11 +243,11 @@ end
 
 (** Int *)
 
-let () = define2 "int_equal" begin fun m n ->
+let () = define2 "int_equal" begin fun _ m n ->
   return (Value.of_bool (Value.to_int m == Value.to_int n))
 end
 
-let binop n f = define2 n begin fun m n ->
+let binop n f = define2 n begin fun _ m n ->
   return (Value.of_int (f (Value.to_int m) (Value.to_int n)))
 end
 
@@ -253,42 +256,42 @@ let () = binop "int_add" (+)
 let () = binop "int_sub" (-)
 let () = binop "int_mul" ( * )
 
-let () = define1 "int_neg" begin fun m ->
+let () = define1 "int_neg" begin fun _ m ->
   return (Value.of_int (~- (Value.to_int m)))
 end
 
 (** String *)
 
-let () = define2 "string_make" begin fun n c ->
+let () = define2 "string_make" begin fun bt n c ->
   let n = Value.to_int n in
   let c = Value.to_char c in
-  if n < 0 || n > Sys.max_string_length then throw err_outofbounds
+  if n < 0 || n > Sys.max_string_length then throw bt err_outofbounds
   else wrap (fun () -> Value.of_string (Bytes.make n c))
 end
 
-let () = define1 "string_length" begin fun s ->
+let () = define1 "string_length" begin fun _ s ->
   return (Value.of_int (Bytes.length (Value.to_string s)))
 end
 
-let () = define3 "string_set" begin fun s n c ->
+let () = define3 "string_set" begin fun bt s n c ->
   let s = Value.to_string s in
   let n = Value.to_int n in
   let c = Value.to_char c in
-  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
   else wrap_unit (fun () -> Bytes.set s n c)
 end
 
-let () = define2 "string_get" begin fun s n ->
+let () = define2 "string_get" begin fun bt s n ->
   let s = Value.to_string s in
   let n = Value.to_int n in
-  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
   else wrap (fun () -> Value.of_char (Bytes.get s n))
 end
 
 (** Terms *)
 
 (** constr -> constr *)
-let () = define1 "constr_type" begin fun c ->
+let () = define1 "constr_type" begin fun bt c ->
   let c = Value.to_constr c in
   let get_type env sigma =
   Proofview.V82.wrap_exceptions begin fun () ->
@@ -296,11 +299,11 @@ let () = define1 "constr_type" begin fun c ->
     let t = Value.of_constr t in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
   end in
-  pf_apply get_type
+  pf_apply bt get_type
 end
 
 (** constr -> constr *)
-let () = define2 "constr_equal" begin fun c1 c2 ->
+let () = define2 "constr_equal" begin fun _ c1 c2 ->
   let c1 = Value.to_constr c1 in
   let c2 = Value.to_constr c2 in
   Proofview.tclEVARMAP >>= fun sigma ->
@@ -308,7 +311,7 @@ let () = define2 "constr_equal" begin fun c1 c2 ->
   Proofview.tclUNIT (Value.of_bool b)
 end
 
-let () = define1 "constr_kind" begin fun c ->
+let () = define1 "constr_kind" begin fun _ c ->
   let open Constr in
   Proofview.tclEVARMAP >>= fun sigma ->
   let c = Value.to_constr c in
@@ -403,7 +406,7 @@ let () = define1 "constr_kind" begin fun c ->
   end
 end
 
-let () = define1 "constr_make" begin fun knd ->
+let () = define1 "constr_make" begin fun _ knd ->
   let open Constr in
   let c = match knd with
   | ValBlk (0, [|n|]) ->
@@ -483,9 +486,9 @@ let () = define1 "constr_make" begin fun knd ->
   return (Value.of_constr c)
 end
 
-let () = define1 "constr_check" begin fun c ->
+let () = define1 "constr_check" begin fun bt c ->
   let c = Value.to_constr c in
-  pf_apply begin fun env sigma ->
+  pf_apply bt begin fun env sigma ->
     try
       let (sigma, _) = Typing.type_of env sigma c in
       Proofview.Unsafe.tclEVARS sigma >>= fun () ->
@@ -496,7 +499,7 @@ let () = define1 "constr_check" begin fun c ->
   end
 end
 
-let () = define3 "constr_substnl" begin fun subst k c ->
+let () = define3 "constr_substnl" begin fun _ subst k c ->
   let subst = Value.to_list Value.to_constr subst in
   let k = Value.to_int k in
   let c = Value.to_constr c in
@@ -504,7 +507,7 @@ let () = define3 "constr_substnl" begin fun subst k c ->
   return (Value.of_constr ans)
 end
 
-let () = define3 "constr_closenl" begin fun ids k c ->
+let () = define3 "constr_closenl" begin fun _ ids k c ->
   let ids = Value.to_list Value.to_ident ids in
   let k = Value.to_int k in
   let c = Value.to_constr c in
@@ -514,16 +517,16 @@ end
 
 (** Patterns *)
 
-let () = define2 "pattern_matches" begin fun pat c ->
+let () = define2 "pattern_matches" begin fun bt pat c ->
   let pat = Value.to_pattern pat in
   let c = Value.to_constr c in
-  pf_apply begin fun env sigma ->
+  pf_apply bt begin fun env sigma ->
     let ans =
       try Some (Constr_matching.matches env sigma pat c)
       with Constr_matching.PatternMatchingFailure -> None
     in
     begin match ans with
-    | None -> Proofview.tclZERO err_matchfailure
+    | None -> Proofview.tclZERO (err_matchfailure bt)
     | Some ans ->
       let ans = Id.Map.bindings ans in
       let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
@@ -532,34 +535,34 @@ let () = define2 "pattern_matches" begin fun pat c ->
   end
 end
 
-let () = define2 "pattern_matches_subterm" begin fun pat c ->
+let () = define2 "pattern_matches_subterm" begin fun bt pat c ->
   let pat = Value.to_pattern pat in
   let c = Value.to_constr c in
   let open Constr_matching in
   let rec of_ans s = match IStream.peek s with
-  | IStream.Nil -> Proofview.tclZERO err_matchfailure
+  | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
   | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
     let ans = Id.Map.bindings sub in
     let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
     let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list of_pair ans |] in
     Proofview.tclOR (return ans) (fun _ -> of_ans s)
   in
-  pf_apply begin fun env sigma ->
+  pf_apply bt begin fun env sigma ->
     let ans = Constr_matching.match_appsubterm env sigma pat c in
     of_ans ans
   end
 end
 
-let () = define2 "pattern_matches_vect" begin fun pat c ->
+let () = define2 "pattern_matches_vect" begin fun bt pat c ->
   let pat = Value.to_pattern pat in
   let c = Value.to_constr c in
-  pf_apply begin fun env sigma ->
+  pf_apply bt begin fun env sigma ->
     let ans =
       try Some (Constr_matching.matches env sigma pat c)
       with Constr_matching.PatternMatchingFailure -> None
     in
     begin match ans with
-    | None -> Proofview.tclZERO err_matchfailure
+    | None -> Proofview.tclZERO (err_matchfailure bt)
     | Some ans ->
       let ans = Id.Map.bindings ans in
       let ans = Array.map_of_list snd ans in
@@ -568,25 +571,25 @@ let () = define2 "pattern_matches_vect" begin fun pat c ->
   end
 end
 
-let () = define2 "pattern_matches_subterm_vect" begin fun pat c ->
+let () = define2 "pattern_matches_subterm_vect" begin fun bt pat c ->
   let pat = Value.to_pattern pat in
   let c = Value.to_constr c in
   let open Constr_matching in
   let rec of_ans s = match IStream.peek s with
-  | IStream.Nil -> Proofview.tclZERO err_matchfailure
+  | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
   | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
     let ans = Id.Map.bindings sub in
     let ans = Array.map_of_list snd ans in
     let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_array Value.of_constr ans |] in
     Proofview.tclOR (return ans) (fun _ -> of_ans s)
   in
-  pf_apply begin fun env sigma ->
+  pf_apply bt begin fun env sigma ->
     let ans = Constr_matching.match_appsubterm env sigma pat c in
     of_ans ans
   end
 end
 
-let () = define2 "pattern_instantiate" begin fun ctx c ->
+let () = define2 "pattern_instantiate" begin fun _ ctx c ->
   let ctx = EConstr.Unsafe.to_constr (Value.to_constr ctx) in
   let c = EConstr.Unsafe.to_constr (Value.to_constr c) in
   let ans = Termops.subst_meta [Constr_matching.special_meta, c] ctx in
@@ -595,46 +598,48 @@ end
 
 (** Error *)
 
-let () = define1 "throw" begin fun e ->
+let () = define1 "throw" begin fun bt e ->
   let (e, info) = Value.to_exn e in
+  let e = set_bt bt e in
   Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
 end
 
 (** Control *)
 
 (** exn -> 'a *)
-let () = define1 "zero" begin fun e ->
+let () = define1 "zero" begin fun bt e ->
   let (e, info) = Value.to_exn e in
+  let e = set_bt bt e in
   Proofview.tclZERO ~info e
 end
 
 (** (unit -> 'a) -> (exn -> 'a) -> 'a *)
-let () = define2 "plus" begin fun x k ->
-  Proofview.tclOR (thaw x) (fun e -> interp_app k [Value.of_exn e])
+let () = define2 "plus" begin fun bt x k ->
+  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt k [Value.of_exn e])
 end
 
 (** (unit -> 'a) -> 'a *)
-let () = define1 "once" begin fun f ->
-  Proofview.tclONCE (thaw f)
+let () = define1 "once" begin fun bt f ->
+  Proofview.tclONCE (thaw bt f)
 end
 
 (** (unit -> unit) list -> unit *)
-let () = define1 "dispatch" begin fun l ->
-  let l = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) l in
+let () = define1 "dispatch" begin fun bt l ->
+  let l = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) l in
   Proofview.tclDISPATCH l >>= fun () -> return v_unit
 end
 
 (** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
-let () = define3 "extend" begin fun lft tac rgt ->
-  let lft = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) lft in
-  let tac = Proofview.tclIGNORE (thaw tac) in
-  let rgt = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
+let () = define3 "extend" begin fun bt lft tac rgt ->
+  let lft = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) lft in
+  let tac = Proofview.tclIGNORE (thaw bt tac) in
+  let rgt = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) rgt in
   Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
 end
 
 (** (unit -> unit) -> unit *)
-let () = define1 "enter" begin fun f ->
-  let f = Proofview.tclIGNORE (thaw f) in
+let () = define1 "enter" begin fun bt f ->
+  let f = Proofview.tclIGNORE (thaw bt f) in
   Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
 end
 
@@ -643,8 +648,8 @@ let e_var = Id.of_string "e"
 let prm_apply_kont_h = pname "apply_kont"
 
 (** (unit -> 'a) -> ('a * ('exn -> 'a)) result *)
-let () = define1 "case" begin fun f ->
-  Proofview.tclCASE (thaw f) >>= begin function
+let () = define1 "case" begin fun bt f ->
+  Proofview.tclCASE (thaw bt f) >>= begin function
   | Proofview.Next (x, k) ->
     let k = {
       clos_ref = None;
@@ -658,38 +663,40 @@ let () = define1 "case" begin fun f ->
 end
 
 (** 'a kont -> exn -> 'a *)
-let () = define2 "apply_kont" begin fun k e ->
-  (Value.to_ext Value.val_kont k) (Value.to_exn e)
+let () = define2 "apply_kont" begin fun bt k e ->
+  let (e, info) = Value.to_exn e in
+  let e = set_bt bt e in
+  (Value.to_ext Value.val_kont k) (e, info)
 end
 
 (** int -> int -> (unit -> 'a) -> 'a *)
-let () = define3 "focus" begin fun i j tac ->
+let () = define3 "focus" begin fun bt i j tac ->
   let i = Value.to_int i in
   let j = Value.to_int j in
-  Proofview.tclFOCUS i j (thaw tac)
+  Proofview.tclFOCUS i j (thaw bt tac)
 end
 
 (** unit -> unit *)
-let () = define0 "shelve" begin
+let () = define0 "shelve" begin fun _ ->
   Proofview.shelve >>= fun () -> return v_unit
 end
 
 (** unit -> unit *)
-let () = define0 "shelve_unifiable" begin
+let () = define0 "shelve_unifiable" begin fun _ ->
   Proofview.shelve_unifiable >>= fun () -> return v_unit
 end
 
-let () = define1 "new_goal" begin fun ev ->
+let () = define1 "new_goal" begin fun bt ev ->
   let ev = Evar.unsafe_of_int (Value.to_int ev) in
   Proofview.tclEVARMAP >>= fun sigma ->
   if Evd.mem sigma ev then
     Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
-  else throw err_notfound
+  else throw bt err_notfound
 end
 
 (** unit -> constr *)
-let () = define0 "goal" begin
-  assert_focussed >>= fun () ->
+let () = define0 "goal" begin fun bt ->
+  assert_focussed bt >>= fun () ->
   Proofview.Goal.enter_one begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
     return (Value.of_constr concl)
@@ -697,9 +704,9 @@ let () = define0 "goal" begin
 end
 
 (** ident -> constr *)
-let () = define1 "hyp" begin fun id ->
+let () = define1 "hyp" begin fun bt id ->
   let id = Value.to_ident id in
-  pf_apply begin fun env _ ->
+  pf_apply bt begin fun env _ ->
     let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in
     if mem then return (Value.of_constr (EConstr.mkVar id))
     else Tacticals.New.tclZEROMSG
@@ -707,8 +714,8 @@ let () = define1 "hyp" begin fun id ->
   end
 end
 
-let () = define0 "hyps" begin
-  pf_apply begin fun env _ ->
+let () = define0 "hyps" begin fun bt ->
+  pf_apply bt begin fun env _ ->
     let open Context.Named.Declaration in
     let hyps = List.rev (Environ.named_context env) in
     let map = function
@@ -725,56 +732,56 @@ let () = define0 "hyps" begin
 end
 
 (** (unit -> constr) -> unit *)
-let () = define1 "refine" begin fun c ->
-  let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
+let () = define1 "refine" begin fun bt c ->
+  let c = thaw bt c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
   Proofview.Goal.nf_enter begin fun gl ->
     Refine.generic_refine ~typecheck:true c gl
   end >>= fun () -> return v_unit
 end
 
-let () = define2 "with_holes" begin fun x f ->
+let () = define2 "with_holes" begin fun bt x f ->
   Proofview.tclEVARMAP >>= fun sigma0 ->
-  thaw x >>= fun ans ->
+  thaw bt x >>= fun ans ->
   Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
-  Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma
+  Tacticals.New.tclWITHHOLES false (Tac2interp.interp_app bt f [ans]) sigma
 end
 
-let () = define1 "progress" begin fun f ->
-  Proofview.tclPROGRESS (thaw f)
+let () = define1 "progress" begin fun bt f ->
+  Proofview.tclPROGRESS (thaw bt f)
 end
 
-let () = define2 "abstract" begin fun id f ->
+let () = define2 "abstract" begin fun bt id f ->
   let id = Value.to_option Value.to_ident id in
-  Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () ->
+  Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw bt f)) >>= fun () ->
   return v_unit
 end
 
-let () = define2 "time" begin fun s f ->
+let () = define2 "time" begin fun bt s f ->
   let s = Value.to_option Value.to_string s in
-  Proofview.tclTIME s (thaw f)
+  Proofview.tclTIME s (thaw bt f)
 end
 
-let () = define0 "check_interrupt" begin
+let () = define0 "check_interrupt" begin fun bt ->
   Proofview.tclCHECKINTERRUPT >>= fun () -> return v_unit
 end
 
 (** Fresh *)
 
-let () = define2 "fresh_free_union" begin fun set1 set2 ->
+let () = define2 "fresh_free_union" begin fun _ set1 set2 ->
   let set1 = Value.to_ext Value.val_free set1 in
   let set2 = Value.to_ext Value.val_free set2 in
   let ans = Id.Set.union set1 set2 in
   return (Value.of_ext Value.val_free ans)
 end
 
-let () = define1 "fresh_free_of_ids" begin fun ids ->
+let () = define1 "fresh_free_of_ids" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   let free = List.fold_right Id.Set.add ids Id.Set.empty in
   return (Value.of_ext Value.val_free free)
 end
 
-let () = define1 "fresh_free_of_constr" begin fun c ->
+let () = define1 "fresh_free_of_constr" begin fun _ c ->
   let c = Value.to_constr c in
   Proofview.tclEVARMAP >>= fun sigma ->
   let rec fold accu c = match EConstr.kind sigma c with
@@ -785,7 +792,7 @@ let () = define1 "fresh_free_of_constr" begin fun c ->
   return (Value.of_ext Value.val_free ans)
 end
 
-let () = define2 "fresh_fresh" begin fun avoid id ->
+let () = define2 "fresh_fresh" begin fun _ avoid id ->
   let avoid = Value.to_ext Value.val_free avoid in
   let id = Value.to_ident id in
   let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in
@@ -828,9 +835,10 @@ let intern_constr self ist c =
 
 let interp_constr flags ist c =
   let open Pretyping in
-  pf_apply begin fun env sigma ->
+  let bt = ist.env_bkt in
+  let ist = to_lvar ist in
+  pf_apply bt begin fun env sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
-    let ist = to_lvar ist in
     let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
     let c = ValExt (Value.val_constr, c) in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
@@ -944,7 +952,7 @@ let () =
 let () =
   let interp ist env sigma concl tac =
     let ist = Tac2interp.get_env ist in
-    let tac = Proofview.tclIGNORE (interp ist tac) in
+    let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
@@ -965,7 +973,9 @@ let () =
   (** FUCK YOU API *)
   let idtac = (Obj.magic idtac : Geninterp.Val.t) in
   let interp ist tac =
-    Tac2interp.interp Tac2interp.empty_environment tac >>= fun _ ->
+    let ist = Tac2interp.get_env ist.Geninterp.lfun in
+    let ist = { ist with env_ist = Id.Map.empty } in
+    Tac2interp.interp ist tac >>= fun _ ->
     Ftactic.return idtac
   in
   Geninterp.register_interp0 wit_ltac2 interp
diff --git a/src/tac2core.mli b/src/tac2core.mli
index 9fae65bb3e..b5800a7172 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -27,4 +27,4 @@ val c_false : ltac_constructor
 
 end
 
-val pf_apply : (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
+val pf_apply : backtrace -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 0754108505..8d515577ec 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -743,6 +743,41 @@ let register_struct ?local str = match str with
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
 | StrMut (qid, e) -> register_redefinition ?local qid e
 
+(** Toplevel exception *)
+
+let print_ltac2_backtrace = ref false
+
+let _ = Goptions.declare_bool_option {
+  Goptions.optdepr = false;
+  Goptions.optname = "print Ltac2 backtrace";
+  Goptions.optkey = ["Ltac2"; "Backtrace"];
+  Goptions.optread = (fun () -> !print_ltac2_backtrace);
+  Goptions.optwrite = (fun b -> print_ltac2_backtrace := b);
+}
+
+let pr_frame = function
+| FrLtac None -> str "<anonymous>"
+| FrLtac (Some kn) ->
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn))
+| FrPrim ml ->
+  str "<" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">"
+| FrExtn (tag, arg) ->
+  let obj = Tac2env.interp_ml_object tag in
+  obj.Tac2env.ml_print (Global.env ()) arg
+
+let () = register_handler begin function
+| Tac2interp.LtacError (kn, _, bt) ->
+  let c = Tac2print.pr_constructor kn in (** FIXME *)
+  let bt =
+    if !print_ltac2_backtrace then
+      fnl () ++ str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt
+    else
+      mt ()
+  in
+  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c) ++ bt
+| _ -> raise Unhandled
+end
+
 (** Printing *)
 
 let print_ltac ref =
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 470323e7c7..36c3fbbe59 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -205,6 +205,16 @@ and closure = {
   (** Global constant from which the closure originates *)
 }
 
-type ml_tactic = valexpr list -> valexpr Proofview.tactic
+type frame =
+| FrLtac of ltac_constant option
+| FrPrim of ml_tactic_name
+| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
 
-type environment = valexpr Id.Map.t
+type backtrace = frame list
+
+type ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
+
+type environment = {
+  env_ist : valexpr Id.Map.t;
+  env_bkt : backtrace;
+}
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index dd20de5ef5..4ed0096787 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -11,7 +11,6 @@ open Globnames
 open Genarg
 open Tac2dyn
 open Tac2expr
-open Tac2interp
 
 (** Dynamic tags *)
 
@@ -98,7 +97,7 @@ let internal_err =
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
-| LtacError (kn, c) -> ValOpn (kn, c)
+| Tac2interp.LtacError (kn, c, _) -> ValOpn (kn, c)
 | _ -> ValOpn (internal_err, [|of_ext val_exn c|])
 
 let to_exn c = match c with
@@ -106,7 +105,7 @@ let to_exn c = match c with
   if Names.KerName.equal kn internal_err then
     to_ext val_exn c.(0)
   else
-    (LtacError (kn, c), Exninfo.null)
+    (Tac2interp.LtacError (kn, c, []), Exninfo.null)
 | _ -> assert false
 
 let of_option f = function
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 7bcfad1be1..b58ce6b851 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -14,25 +14,19 @@ open Names
 open Proofview.Notations
 open Tac2expr
 
-exception LtacError of KerName.t * valexpr array
+exception LtacError of KerName.t * valexpr array * backtrace
 
-let () = register_handler begin function
-| LtacError (kn, _) ->
-  let c = Tac2print.pr_constructor kn in
-  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
-| _ -> raise Unhandled
-end
-
-type environment = valexpr Id.Map.t
-
-let empty_environment = Id.Map.empty
+let empty_environment = {
+  env_ist = Id.Map.empty;
+  env_bkt = [];
+}
 
 let push_name ist id v = match id with
 | Anonymous -> ist
-| Name id -> Id.Map.add id v ist
+| Name id -> { ist with env_ist = Id.Map.add id v ist.env_ist }
 
 let get_var ist id =
-  try Id.Map.find id ist with Not_found ->
+  try Id.Map.find id ist.env_ist with Not_found ->
     anomaly (str "Unbound variable " ++ Id.print id)
 
 let get_ref ist kn =
@@ -41,18 +35,18 @@ let get_ref ist kn =
 
 let return = Proofview.tclUNIT
 
-let rec interp ist = function
+let rec interp (ist : environment) = function
 | GTacAtm (AtmInt n) -> return (ValInt n)
 | GTacAtm (AtmStr s) -> return (ValStr (Bytes.of_string s))
 | GTacVar id -> return (get_var ist id)
 | GTacRef qid -> return (get_ref ist qid)
 | GTacFun (ids, e) ->
-  let cls = { clos_ref = None; clos_env = ist; clos_var = ids; clos_exp = e } in
+  let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
   return (ValCls cls)
 | GTacApp (f, args) ->
   interp ist f >>= fun f ->
   Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
-  interp_app f args
+  interp_app ist.env_bkt f args
 | GTacLet (false, el, e) ->
   let fold accu (na, e) =
     interp ist e >>= fun e ->
@@ -63,18 +57,18 @@ let rec interp ist = function
 | GTacLet (true, el, e) ->
   let map (na, e) = match e with
   | GTacFun (ids, e) ->
-    let cls = { clos_ref = None; clos_env = ist; clos_var = ids; clos_exp = e } in
+    let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
     na, cls
   | _ -> anomaly (str "Ill-formed recursive function")
   in
   let fixs = List.map map el in
   let fold accu (na, cls) = match na with
   | Anonymous -> accu
-  | Name id -> Id.Map.add id (ValCls cls) accu
+  | Name id -> { ist with env_ist = Id.Map.add id (ValCls cls) accu.env_ist }
   in
   let ist = List.fold_left fold ist fixs in
   (** Hack to make a cycle imperatively in the environment *)
-  let iter (_, e) = e.clos_env <- ist in
+  let iter (_, e) = e.clos_env <- ist.env_ist in
   let () = List.iter iter fixs in
   interp ist e
 | GTacCst (_, n, []) -> return (ValInt n)
@@ -96,22 +90,23 @@ let rec interp ist = function
   return (ValOpn (kn, Array.of_list el))
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
-  Tac2env.interp_primitive ml el
+  Tac2env.interp_primitive ml (FrPrim ml :: ist.env_bkt) el
 | GTacExt (tag, e) ->
   let tpe = Tac2env.interp_ml_object tag in
+  let ist = { ist with env_bkt = FrExtn (tag, e) :: ist.env_bkt } in
   tpe.Tac2env.ml_interp ist e
 
-and interp_app f args = match f with
+and interp_app bt f args = match f with
 | ValCls { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } ->
   let rec push ist ids args = match ids, args with
   | [], [] -> interp ist e
-  | [], _ :: _ -> interp ist e >>= fun f -> interp_app f args
+  | [], _ :: _ -> interp ist e >>= fun f -> interp_app bt f args
   | _ :: _, [] ->
-    let cls = { clos_ref = kn; clos_env = ist; clos_var = ids; clos_exp = e } in
+    let cls = { clos_ref = kn; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
     return (ValCls cls)
   | id :: ids, arg :: args -> push (push_name ist id arg) ids args
   in
-  push ist ids args
+  push { env_ist = ist; env_bkt = FrLtac kn :: bt } ids args
 | ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
 
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 1ac26b48db..ea7db33b60 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -9,13 +9,11 @@
 open Names
 open Tac2expr
 
-type environment = valexpr Id.Map.t
-
 val empty_environment : environment
 
 val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
-val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic
+val interp_app : backtrace -> valexpr -> valexpr list -> valexpr Proofview.tactic
 
 (** {5 Cross-boundary encodings} *)
 
@@ -24,5 +22,5 @@ val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound
 
 (** {5 Exceptions} *)
 
-exception LtacError of KerName.t * valexpr array
+exception LtacError of KerName.t * valexpr array * backtrace
 (** Ltac2-defined exceptions seen from OCaml side *)
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 2a57fdc705..6dcb3f15fb 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -18,7 +18,7 @@ module Value = Tac2ffi
 
 let return x = Proofview.tclUNIT x
 let v_unit = Value.of_unit ()
-let thaw f = Tac2interp.interp_app f [v_unit]
+let thaw bt f = Tac2interp.interp_app bt f [v_unit]
 
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)
@@ -126,7 +126,8 @@ and to_intro_patterns il =
 
 let to_destruction_arg = function
 | ValBlk (0, [| c |]) ->
-  let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  (** FIXME: lost backtrace *)
+  let c = thaw [] c >>= fun c -> return (to_constr_with_bindings c) in
   ElimOnConstr c
 | ValBlk (1, [| id |]) -> ElimOnIdent (Loc.tag (Value.to_ident id))
 | ValBlk (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
@@ -153,7 +154,8 @@ let to_rewriting = function
 | ValBlk (0, [| orient; repeat; c |]) ->
   let orient = Value.to_option Value.to_bool orient in
   let repeat = to_multi repeat in
-  let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  (** FIXME: lost backtrace *)
+  let c = thaw [] c >>= fun c -> return (to_constr_with_bindings c) in
   (orient, repeat, c)
 | _ -> assert false
 
@@ -164,52 +166,52 @@ let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 let lift tac = tac <*> return v_unit
 
 let define_prim0 name tac =
-  let tac = function
+  let tac bt arg = match arg with
   | [_] -> lift tac
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_prim1 name tac =
-  let tac = function
-  | [x] -> lift (tac x)
+  let tac bt arg = match arg with
+  | [x] -> lift (tac bt x)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_prim2 name tac =
-  let tac = function
-  | [x; y] -> lift (tac x y)
+  let tac bt arg = match arg with
+  | [x; y] -> lift (tac bt x y)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_prim3 name tac =
-  let tac = function
-  | [x; y; z] -> lift (tac x y z)
+  let tac bt arg = match arg with
+  | [x; y; z] -> lift (tac bt x y z)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_prim4 name tac =
-  let tac = function
-  | [x; y; z; u] -> lift (tac x y z u)
+  let tac bt arg = match arg with
+  | [x; y; z; u] -> lift (tac bt x y z u)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 (** Tactics from Tacexpr *)
 
-let () = define_prim2 "tac_intros" begin fun ev ipat ->
+let () = define_prim2 "tac_intros" begin fun _ ev ipat ->
   let ev = Value.to_bool ev in
   let ipat = to_intro_patterns ipat in
   Tactics.intros_patterns ev ipat
 end
 
-let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
+let () = define_prim4 "tac_apply" begin fun bt adv ev cb ipat ->
   let adv = Value.to_bool adv in
   let ev = Value.to_bool ev in
-  let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  let map_cb c = thaw bt c >>= fun c -> return (to_constr_with_bindings c) in
   let cb = Value.to_list map_cb cb in
   let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in
   let map_ipat p = to_pair Value.to_ident map p in
@@ -217,20 +219,20 @@ let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
   Tac2tactics.apply adv ev cb ipat
 end
 
-let () = define_prim3 "tac_elim" begin fun ev c copt ->
+let () = define_prim3 "tac_elim" begin fun _ ev c copt ->
   let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
   let copt = Value.to_option to_constr_with_bindings copt in
   Tactics.elim ev None c copt
 end
 
-let () = define_prim2 "tac_case" begin fun ev c ->
+let () = define_prim2 "tac_case" begin fun _ ev c ->
   let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
   Tactics.general_case_analysis ev None c
 end
 
-let () = define_prim1 "tac_generalize" begin fun cl ->
+let () = define_prim1 "tac_generalize" begin fun _ cl ->
   let cast = function
   | ValBlk (0, [| c; occs; na |]) ->
     ((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
@@ -240,113 +242,113 @@ let () = define_prim1 "tac_generalize" begin fun cl ->
   Tactics.new_generalize_gen cl
 end
 
-let () = define_prim3 "tac_assert" begin fun c tac ipat ->
+let () = define_prim3 "tac_assert" begin fun bt c tac ipat ->
   let c = Value.to_constr c in
-  let of_tac t = Proofview.tclIGNORE (thaw t) in
+  let of_tac t = Proofview.tclIGNORE (thaw bt t) in
   let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
   let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
   Tactics.forward true tac ipat c
 end
 
-let () = define_prim3 "tac_enough" begin fun c tac ipat ->
+let () = define_prim3 "tac_enough" begin fun bt c tac ipat ->
   let c = Value.to_constr c in
-  let of_tac t = Proofview.tclIGNORE (thaw t) in
+  let of_tac t = Proofview.tclIGNORE (thaw bt t) in
   let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
   let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
   Tactics.forward false tac ipat c
 end
 
-let () = define_prim2 "tac_pose" begin fun idopt c ->
+let () = define_prim2 "tac_pose" begin fun _ idopt c ->
   let na = to_name idopt in
   let c = Value.to_constr c in
   Tactics.letin_tac None na c None Locusops.nowhere
 end
 
-let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
+let () = define_prim4 "tac_set" begin fun bt ev idopt c cl ->
   let ev = Value.to_bool ev in
   let na = to_name idopt in
   let cl = to_clause cl in
   Proofview.tclEVARMAP >>= fun sigma ->
-  thaw c >>= fun c ->
+  thaw bt c >>= fun c ->
   let c = Value.to_constr c in
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
-let () = define_prim3 "tac_destruct" begin fun ev ic using ->
+let () = define_prim3 "tac_destruct" begin fun _ ev ic using ->
   let ev = Value.to_bool ev in
   let ic = Value.to_list to_induction_clause ic in
   let using = Value.to_option to_constr_with_bindings using in
   Tac2tactics.induction_destruct false ev ic using
 end
 
-let () = define_prim3 "tac_induction" begin fun ev ic using ->
+let () = define_prim3 "tac_induction" begin fun _ ev ic using ->
   let ev = Value.to_bool ev in
   let ic = Value.to_list to_induction_clause ic in
   let using = Value.to_option to_constr_with_bindings using in
   Tac2tactics.induction_destruct true ev ic using
 end
 
-let () = define_prim1 "tac_red" begin fun cl ->
+let () = define_prim1 "tac_red" begin fun _ cl ->
   let cl = to_clause cl in
   Tactics.reduce (Red false) cl
 end
 
-let () = define_prim1 "tac_hnf" begin fun cl ->
+let () = define_prim1 "tac_hnf" begin fun _ cl ->
   let cl = to_clause cl in
   Tactics.reduce Hnf cl
 end
 
-let () = define_prim3 "tac_simpl" begin fun flags where cl ->
+let () = define_prim3 "tac_simpl" begin fun _ flags where cl ->
   let flags = to_red_flag flags in
   let where = Value.to_option to_pattern_with_occs where in
   let cl = to_clause cl in
   Tac2tactics.simpl flags where cl
 end
 
-let () = define_prim2 "tac_cbv" begin fun flags cl ->
+let () = define_prim2 "tac_cbv" begin fun _ flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
   Tac2tactics.cbv flags cl
 end
 
-let () = define_prim2 "tac_cbn" begin fun flags cl ->
+let () = define_prim2 "tac_cbn" begin fun _ flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
   Tac2tactics.cbn flags cl
 end
 
-let () = define_prim2 "tac_lazy" begin fun flags cl ->
+let () = define_prim2 "tac_lazy" begin fun _ flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
   Tac2tactics.lazy_ flags cl
 end
 
-let () = define_prim2 "tac_unfold" begin fun refs cl ->
+let () = define_prim2 "tac_unfold" begin fun _ refs cl ->
   let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
   let refs = Value.to_list map refs in
   let cl = to_clause cl in
   Tac2tactics.unfold refs cl
 end
 
-let () = define_prim2 "tac_fold" begin fun args cl ->
+let () = define_prim2 "tac_fold" begin fun _ args cl ->
   let args = Value.to_list Value.to_constr args in
   let cl = to_clause cl in
   Tactics.reduce (Fold args) cl
 end
 
-let () = define_prim2 "tac_pattern" begin fun where cl ->
+let () = define_prim2 "tac_pattern" begin fun _ where cl ->
   let where = Value.to_list to_constr_with_occs where in
   let cl = to_clause cl in
   Tactics.reduce (Pattern where) cl
 end
 
-let () = define_prim2 "tac_vm" begin fun where cl ->
+let () = define_prim2 "tac_vm" begin fun _ where cl ->
   let where = Value.to_option to_pattern_with_occs where in
   let cl = to_clause cl in
   Tac2tactics.vm where cl
 end
 
-let () = define_prim2 "tac_native" begin fun where cl ->
+let () = define_prim2 "tac_native" begin fun _ where cl ->
   let where = Value.to_option to_pattern_with_occs where in
   let cl = to_clause cl in
   Tac2tactics.native where cl
@@ -355,97 +357,97 @@ end
 (** Reduction functions *)
 
 let define_red1 name tac =
-  let tac = function
-  | [x] -> tac x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  let tac bt arg = match arg with
+  | [x] -> tac bt x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_red2 name tac =
-  let tac = function
-  | [x; y] -> tac x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  let tac bt arg = match arg with
+  | [x; y] -> tac bt x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
 let define_red3 name tac =
-  let tac = function
-  | [x; y; z] -> tac x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  let tac bt arg = match arg with
+  | [x; y; z] -> tac bt x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
   | _ -> assert false
   in
   Tac2env.define_primitive (pname name) tac
 
-let () = define_red1 "eval_red" begin fun c ->
+let () = define_red1 "eval_red" begin fun bt c ->
   let c = Value.to_constr c in
-  Tac2tactics.eval_red c
+  Tac2tactics.eval_red bt c
 end
 
-let () = define_red1 "eval_hnf" begin fun c ->
+let () = define_red1 "eval_hnf" begin fun bt c ->
   let c = Value.to_constr c in
-  Tac2tactics.eval_hnf c
+  Tac2tactics.eval_hnf bt c
 end
 
-let () = define_red3 "eval_simpl" begin fun flags where c ->
+let () = define_red3 "eval_simpl" begin fun bt flags where c ->
   let flags = to_red_flag flags in
   let where = Value.to_option to_pattern_with_occs where in
   let c = Value.to_constr c in
-  Tac2tactics.eval_simpl flags where c
+  Tac2tactics.eval_simpl bt flags where c
 end
 
-let () = define_red2 "eval_cbv" begin fun flags c ->
+let () = define_red2 "eval_cbv" begin fun bt flags c ->
   let flags = to_red_flag flags in
   let c = Value.to_constr c in
-  Tac2tactics.eval_cbv flags c
+  Tac2tactics.eval_cbv bt flags c
 end
 
-let () = define_red2 "eval_cbn" begin fun flags c ->
+let () = define_red2 "eval_cbn" begin fun bt flags c ->
   let flags = to_red_flag flags in
   let c = Value.to_constr c in
-  Tac2tactics.eval_cbn flags c
+  Tac2tactics.eval_cbn bt flags c
 end
 
-let () = define_red2 "eval_lazy" begin fun flags c ->
+let () = define_red2 "eval_lazy" begin fun bt flags c ->
   let flags = to_red_flag flags in
   let c = Value.to_constr c in
-  Tac2tactics.eval_lazy flags c
+  Tac2tactics.eval_lazy bt flags c
 end
 
-let () = define_red2 "eval_unfold" begin fun refs c ->
+let () = define_red2 "eval_unfold" begin fun bt refs c ->
   let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
   let refs = Value.to_list map refs in
   let c = Value.to_constr c in
-  Tac2tactics.eval_unfold refs c
+  Tac2tactics.eval_unfold bt refs c
 end
 
-let () = define_red2 "eval_fold" begin fun args c ->
+let () = define_red2 "eval_fold" begin fun bt args c ->
   let args = Value.to_list Value.to_constr args in
   let c = Value.to_constr c in
-  Tac2tactics.eval_fold args c
+  Tac2tactics.eval_fold bt args c
 end
 
-let () = define_red2 "eval_pattern" begin fun where c ->
+let () = define_red2 "eval_pattern" begin fun bt where c ->
   let where = Value.to_list (fun p -> to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) p) where in
   let c = Value.to_constr c in
-  Tac2tactics.eval_pattern where c
+  Tac2tactics.eval_pattern bt where c
 end
 
-let () = define_red2 "eval_vm" begin fun where c ->
+let () = define_red2 "eval_vm" begin fun bt where c ->
   let where = Value.to_option to_pattern_with_occs where in
   let c = Value.to_constr c in
-  Tac2tactics.eval_vm where c
+  Tac2tactics.eval_vm bt where c
 end
 
-let () = define_red2 "eval_native" begin fun where c ->
+let () = define_red2 "eval_native" begin fun bt where c ->
   let where = Value.to_option to_pattern_with_occs where in
   let c = Value.to_constr c in
-  Tac2tactics.eval_native where c
+  Tac2tactics.eval_native bt where c
 end
 
-let () = define_prim4 "tac_rewrite" begin fun ev rw cl by ->
+let () = define_prim4 "tac_rewrite" begin fun bt ev rw cl by ->
   let ev = Value.to_bool ev in
   let rw = Value.to_list to_rewriting rw in
   let cl = to_clause cl in
-  let to_tac t = Proofview.tclIGNORE (thaw t) in
+  let to_tac t = Proofview.tclIGNORE (thaw bt t) in
   let by = Value.to_option to_tac by in
   Tac2tactics.rewrite ev rw cl by
 end
@@ -464,69 +466,69 @@ END
 
 let () = define_prim0 "tac_assumption" Tactics.assumption
 
-let () = define_prim1 "tac_transitivity" begin fun c ->
+let () = define_prim1 "tac_transitivity" begin fun _ c ->
   let c = Value.to_constr c in
   Tactics.intros_transitivity (Some c)
 end
 
 let () = define_prim0 "tac_etransitivity" (Tactics.intros_transitivity None)
 
-let () = define_prim1 "tac_cut" begin fun c ->
+let () = define_prim1 "tac_cut" begin fun _ c ->
   let c = Value.to_constr c in
   Tactics.cut c
 end
 
-let () = define_prim2 "tac_left" begin fun ev bnd ->
+let () = define_prim2 "tac_left" begin fun _ ev bnd ->
   let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
   Tactics.left_with_bindings ev bnd
 end
-let () = define_prim2 "tac_right" begin fun ev bnd ->
+let () = define_prim2 "tac_right" begin fun _ ev bnd ->
   let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
   Tactics.right_with_bindings ev bnd
 end
 
-let () = define_prim1 "tac_introsuntil" begin fun h ->
+let () = define_prim1 "tac_introsuntil" begin fun _ h ->
   Tactics.intros_until (to_qhyp h)
 end
 
-let () = define_prim1 "tac_exactnocheck" begin fun c ->
+let () = define_prim1 "tac_exactnocheck" begin fun _ c ->
   Tactics.exact_no_check (Value.to_constr c)
 end
 
-let () = define_prim1 "tac_vmcastnocheck" begin fun c ->
+let () = define_prim1 "tac_vmcastnocheck" begin fun _ c ->
   Tactics.vm_cast_no_check (Value.to_constr c)
 end
 
-let () = define_prim1 "tac_nativecastnocheck" begin fun c ->
+let () = define_prim1 "tac_nativecastnocheck" begin fun _ c ->
   Tactics.native_cast_no_check (Value.to_constr c)
 end
 
-let () = define_prim1 "tac_constructor" begin fun ev ->
+let () = define_prim1 "tac_constructor" begin fun _ ev ->
   let ev = Value.to_bool ev in
   Tactics.any_constructor ev None
 end
 
-let () = define_prim3 "tac_constructorn" begin fun ev n bnd ->
+let () = define_prim3 "tac_constructorn" begin fun _ ev n bnd ->
   let ev = Value.to_bool ev in
   let n = Value.to_int n in
   let bnd = to_bindings bnd in
   Tactics.constructor_tac ev None n bnd
 end
 
-let () = define_prim1 "tac_symmetry" begin fun cl ->
+let () = define_prim1 "tac_symmetry" begin fun _ cl ->
   let cl = to_clause cl in
   Tactics.intros_symmetry cl
 end
 
-let () = define_prim2 "tac_split" begin fun ev bnd ->
+let () = define_prim2 "tac_split" begin fun _ ev bnd ->
   let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
   Tactics.split_with_bindings ev [bnd]
 end
 
-let () = define_prim1 "tac_rename" begin fun ids ->
+let () = define_prim1 "tac_rename" begin fun _ ids ->
   let map c = match Value.to_tuple c with
   | [|x; y|] -> (Value.to_ident x, Value.to_ident y)
   | _ -> assert false
@@ -535,72 +537,72 @@ let () = define_prim1 "tac_rename" begin fun ids ->
   Tactics.rename_hyp ids
 end
 
-let () = define_prim1 "tac_revert" begin fun ids ->
+let () = define_prim1 "tac_revert" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   Tactics.revert ids
 end
 
 let () = define_prim0 "tac_admit" Proofview.give_up
 
-let () = define_prim2 "tac_fix" begin fun idopt n ->
+let () = define_prim2 "tac_fix" begin fun _ idopt n ->
   let idopt = Value.to_option Value.to_ident idopt in
   let n = Value.to_int n in
   Tactics.fix idopt n
 end
 
-let () = define_prim1 "tac_cofix" begin fun idopt ->
+let () = define_prim1 "tac_cofix" begin fun _ idopt ->
   let idopt = Value.to_option Value.to_ident idopt in
   Tactics.cofix idopt
 end
 
-let () = define_prim1 "tac_clear" begin fun ids ->
+let () = define_prim1 "tac_clear" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   Tactics.clear ids
 end
 
-let () = define_prim1 "tac_keep" begin fun ids ->
+let () = define_prim1 "tac_keep" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   Tactics.keep ids
 end
 
-let () = define_prim1 "tac_clearbody" begin fun ids ->
+let () = define_prim1 "tac_clearbody" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   Tactics.clear_body ids
 end
 
 (** Tactics from extratactics *)
 
-let () = define_prim2 "tac_discriminate" begin fun ev arg ->
+let () = define_prim2 "tac_discriminate" begin fun _ ev arg ->
   let ev = Value.to_bool ev in
   let arg = Value.to_option (fun arg -> None, to_destruction_arg arg) arg in
   Tac2tactics.discriminate ev arg
 end
 
-let () = define_prim3 "tac_injection" begin fun ev ipat arg ->
+let () = define_prim3 "tac_injection" begin fun _ ev ipat arg ->
   let ev = Value.to_bool ev in
   let ipat = Value.to_option to_intro_patterns ipat in
   let arg = Value.to_option (fun arg -> None, to_destruction_arg arg) arg in
   Tac2tactics.injection ev ipat arg
 end
 
-let () = define_prim1 "tac_absurd" begin fun c ->
+let () = define_prim1 "tac_absurd" begin fun _ c ->
   Contradiction.absurd (Value.to_constr c)
 end
 
-let () = define_prim1 "tac_contradiction" begin fun c ->
+let () = define_prim1 "tac_contradiction" begin fun _ c ->
   let c = Value.to_option to_constr_with_bindings c in
   Contradiction.contradiction c
 end
 
-let () = define_prim4 "tac_autorewrite" begin fun all by ids cl ->
+let () = define_prim4 "tac_autorewrite" begin fun bt all by ids cl ->
   let all = Value.to_bool all in
-  let by = Value.to_option (fun tac -> Proofview.tclIGNORE (thaw tac)) by in
+  let by = Value.to_option (fun tac -> Proofview.tclIGNORE (thaw bt tac)) by in
   let ids = Value.to_list Value.to_ident ids in
   let cl = to_clause cl in
   Tac2tactics.autorewrite ~all by ids cl
 end
 
-let () = define_prim1 "tac_subst" begin fun ids ->
+let () = define_prim1 "tac_subst" begin fun _ ids ->
   let ids = Value.to_list Value.to_ident ids in
   Equality.subst ids
 end
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index a95e60bc97..5b35d53be4 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -122,62 +122,62 @@ let native where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvNative where) cl
 
-let eval_fun red c =
-  Tac2core.pf_apply begin fun env sigma ->
+let eval_fun bt red c =
+  Tac2core.pf_apply bt begin fun env sigma ->
   let (redfun, _) = Redexpr.reduction_of_red_expr env red in
   let (sigma, ans) = redfun env sigma c in
   Proofview.Unsafe.tclEVARS sigma >>= fun () ->
   Proofview.tclUNIT ans
   end
 
-let eval_red c =
-  eval_fun (Red false) c
+let eval_red bt c =
+  eval_fun bt (Red false) c
 
-let eval_hnf c =
-  eval_fun Hnf c
+let eval_hnf bt c =
+  eval_fun bt Hnf c
 
-let eval_simpl flags where c =
+let eval_simpl bt flags where c =
   let where = Option.map map_pattern_with_occs where in
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
-  eval_fun (Simpl (flags, where)) c
+  eval_fun bt (Simpl (flags, where)) c
 
-let eval_cbv flags c =
+let eval_cbv bt flags c =
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
-  eval_fun (Cbv flags) c
+  eval_fun bt (Cbv flags) c
 
-let eval_cbn flags c =
+let eval_cbn bt flags c =
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
-  eval_fun (Cbn flags) c
+  eval_fun bt (Cbn flags) c
 
-let eval_lazy flags c =
+let eval_lazy bt flags c =
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
-  eval_fun (Lazy flags) c
+  eval_fun bt (Lazy flags) c
 
-let eval_unfold occs c =
+let eval_unfold bt occs c =
   let map (gr, occ) =
     get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
   in
   Proofview.Monad.List.map map occs >>= fun occs ->
-  eval_fun (Unfold occs) c
+  eval_fun bt (Unfold occs) c
 
-let eval_fold cl c =
-  eval_fun (Fold cl) c
+let eval_fold bt cl c =
+  eval_fun bt (Fold cl) c
 
-let eval_pattern where c =
+let eval_pattern bt where c =
   let where = List.map (fun (pat, occ) -> (occ, pat)) where in
-  eval_fun (Pattern where) c
+  eval_fun bt (Pattern where) c
 
-let eval_vm where c =
+let eval_vm bt where c =
   let where = Option.map map_pattern_with_occs where in
-  eval_fun (CbvVm where) c
+  eval_fun bt (CbvVm where) c
 
-let eval_native where c =
+let eval_native bt where c =
   let where = Option.map map_pattern_with_occs where in
-  eval_fun (CbvNative where) c
+  eval_fun bt (CbvNative where) c
 
 let on_destruction_arg tac ev arg =
   Proofview.Goal.enter begin fun gl ->
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 87489bb248..1c76bd9648 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -9,6 +9,7 @@
 open Names
 open Locus
 open Globnames
+open Tac2expr
 open EConstr
 open Genredexpr
 open Misctypes
@@ -55,28 +56,28 @@ val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit ta
 
 val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
-val eval_red : constr -> constr tactic
+val eval_red : backtrace -> constr -> constr tactic
 
-val eval_hnf : constr -> constr tactic
+val eval_hnf : backtrace -> constr -> constr tactic
 
-val eval_simpl : global_reference glob_red_flag ->
+val eval_simpl : backtrace -> global_reference glob_red_flag ->
   (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
 
-val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbv : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
 
-val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbn : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
 
-val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
+val eval_lazy : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
 
-val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
+val eval_unfold : backtrace -> (global_reference * occurrences_expr) list -> constr -> constr tactic
 
-val eval_fold : constr list -> constr -> constr tactic
+val eval_fold : backtrace -> constr list -> constr -> constr tactic
 
-val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+val eval_pattern : backtrace -> (EConstr.t * occurrences_expr) list -> constr -> constr tactic
 
-val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_vm : backtrace -> (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
 
-val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_native : backtrace -> (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
 
 val discriminate : evars_flag -> destruction_arg option -> unit tactic