Moving Ltac2 backtraces to the Exninfo mechanism.

I don't know why, but on CoqIDE this triggers a printing of the backtrace
twice. This is not reproducible with coqtop.

6 files changed, 45 insertions, 38 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index e01b9f3086..ab87fa7739 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -87,17 +87,17 @@ let of_result f = function
 
 (** Stdlib exceptions *)
 
-let err_notfocussed bt =
-  Tac2interp.LtacError (coq_core "Not_focussed", [||], bt)
+let err_notfocussed =
+  Tac2interp.LtacError (coq_core "Not_focussed", [||])
 
-let err_outofbounds bt =
-  Tac2interp.LtacError (coq_core "Out_of_bounds", [||], bt)
+let err_outofbounds =
+  Tac2interp.LtacError (coq_core "Out_of_bounds", [||])
 
-let err_notfound bt =
-  Tac2interp.LtacError (coq_core "Not_found", [||], bt)
+let err_notfound =
+  Tac2interp.LtacError (coq_core "Not_found", [||])
 
-let err_matchfailure bt =
-  Tac2interp.LtacError (coq_core "Match_failure", [||], bt)
+let err_matchfailure =
+  Tac2interp.LtacError (coq_core "Match_failure", [||])
 
 (** Helper functions *)
 
@@ -106,16 +106,18 @@ let thaw f = f [v_unit]
 let fatal_flag : unit Exninfo.t = Exninfo.make ()
 let fatal_info = Exninfo.add Exninfo.null fatal_flag ()
 
-let throw e =
+let set_bt info =
   Tac2interp.get_backtrace >>= fun bt ->
-  Proofview.tclLIFT (Proofview.NonLogical.raise ~info:fatal_info (e bt))
+  Proofview.tclUNIT (Exninfo.add info Tac2entries.backtrace bt)
 
-let fail e =
-  Tac2interp.get_backtrace >>= fun bt -> Proofview.tclZERO (e bt)
+let throw ?(info = Exninfo.null) e =
+  set_bt info >>= fun info ->
+  let info = Exninfo.add info fatal_flag () in
+  Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
 
-let set_bt bt e = match e with
-| Tac2interp.LtacError (kn, args, _) -> Tac2interp.LtacError (kn, args, bt)
-| e -> e
+let fail ?(info = Exninfo.null) e =
+  set_bt info >>= fun info ->
+  Proofview.tclZERO ~info e
 
 let return x = Proofview.tclUNIT x
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -572,19 +574,14 @@ end
 (** Error *)
 
 let () = define1 "throw" exn begin fun (e, info) ->
-  Tac2interp.get_backtrace >>= fun bt ->
-  let e = set_bt bt e in
-  let info = Exninfo.add info fatal_flag () in
-  Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+  throw ~info e
 end
 
 (** Control *)
 
 (** exn -> 'a *)
 let () = define1 "zero" exn begin fun (e, info) ->
-  Tac2interp.get_backtrace >>= fun bt ->
-  let e = set_bt bt e in
-  Proofview.tclZERO ~info e
+  fail ~info e
 end
 
 (** (unit -> 'a) -> (exn -> 'a) -> 'a *)
@@ -624,8 +621,7 @@ let () = define1 "case" closure begin fun f ->
     let k = function
     | [e] ->
       let (e, info) = Value.to_exn e in
-      Tac2interp.get_backtrace >>= fun bt ->
-      let e = set_bt bt e in
+      set_bt info >>= fun info ->
       k (e, info)
     | _ -> assert false
     in
@@ -805,7 +801,7 @@ let interp_constr flags ist c =
     let (e, info) = CErrors.push e in
     match Exninfo.get info fatal_flag with
     | None -> Proofview.tclZERO ~info e
-    | Some () -> Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+    | Some () -> throw ~info e
   end
 
 let () =
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 9a2693379b..208231b814 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -756,6 +756,8 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b);
 }
 
+let backtrace : backtrace Exninfo.t = Exninfo.make ()
+
 let pr_frame = function
 | FrAnon e -> str "Call {" ++ pr_glbexpr e ++ str "}"
 | FrLtac kn ->
@@ -768,21 +770,26 @@ let pr_frame = function
     obj.Tac2env.ml_print (Global.env ()) arg
 
 let () = register_handler begin function
-| Tac2interp.LtacError (kn, args, bt) ->
+| Tac2interp.LtacError (kn, args) ->
   let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
   let v = ValOpn (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
-  let bt =
-    if !Tac2interp.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
+  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
 | _ -> raise Unhandled
 end
 
+let () = ExplainErr.register_additional_error_info begin fun (e, info) ->
+  if !Tac2interp.print_ltac2_backtrace then
+    let bt = Exninfo.get info backtrace in
+    let bt = Option.default [] bt in
+    let bt =
+      str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl ()
+    in
+    Some (Loc.tag @@ Some bt)
+  else raise Exit
+end
+
 (** Printing *)
 
 let print_ltac ref =
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index dda1653593..7c71130402 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -49,6 +49,10 @@ val print_ltac : Libnames.reference -> unit
 (** Evaluate a tactic expression in the current environment *)
 val call : default:bool -> raw_tacexpr -> unit
 
+(** {5 Toplevel exceptions} *)
+
+val backtrace : backtrace Exninfo.t
+
 (** {5 Parsing entries} *)
 
 module Pltac :
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index fb97177c4d..16c17cce62 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -43,7 +43,7 @@ match Val.eq tag tag' with
 
 (** Exception *)
 
-exception LtacError of KerName.t * valexpr array * backtrace
+exception LtacError of KerName.t * valexpr array
 
 (** Conversion functions *)
 
@@ -169,7 +169,7 @@ let internal_err =
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
-| LtacError (kn, c, _) -> ValOpn (kn, c)
+| LtacError (kn, c) -> ValOpn (kn, c)
 | _ -> ValOpn (internal_err, [|of_ext val_exn c|])
 
 let to_exn c = match c with
@@ -177,7 +177,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)
+    (LtacError (kn, c), Exninfo.null)
 | _ -> assert false
 
 let exn = {
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index dfc87f7db3..05f4d210ab 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -121,5 +121,5 @@ val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 
 (** Exception *)
 
-exception LtacError of KerName.t * valexpr array * backtrace
+exception LtacError of KerName.t * valexpr array
 (** Ltac2-defined exceptions seen from OCaml side *)
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 1003e9f1eb..3acca72367 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -22,7 +22,7 @@ val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound
 
 (** {5 Exceptions} *)
 
-exception LtacError of KerName.t * valexpr array * backtrace
+exception LtacError of KerName.t * valexpr array
 (** Ltac2-defined exceptions seen from OCaml side *)
 
 (** {5 Backtrace} *)