[ocaml] Remove Custom Backtrace module in favor of OCaml's

As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .

In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.

Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.

We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.

Closes #6446

Example with backtrace from https://github.com/coq/coq/issues/11366

Old:

```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```

New:

```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```

4 files changed, 74 insertions, 225 deletions

diff --git a/clib/backtrace.ml b/clib/backtrace.ml
deleted file mode 100644
index 81803a81a5..0000000000
--- a/clib/backtrace.ml
+++ /dev/null
@@ -1,119 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-[@@@ocaml.warning "-37"]
-
-type raw_frame =
-| Known_location of bool   (* is_raise *)
-  * string (* filename *)
-  * int    (* line number *)
-  * int    (* start char *)
-  * int    (* end char *)
-| Unknown_location of bool (*is_raise*)
-
-type location = {
-  loc_filename : string;
-  loc_line : int;
-  loc_start : int;
-  loc_end : int;
-}
-
-type frame = { frame_location : location option; frame_raised : bool; }
-
-external get_exception_backtrace: unit -> raw_frame array option
-  = "caml_get_exception_backtrace"
-
-type t = raw_frame array list
-(** List of partial raw stack frames, in reverse order *)
-
-let empty = []
-
-let of_raw = function
-| Unknown_location r ->
-  { frame_location = None; frame_raised = r; }
-| Known_location (r, file, line, st, en) ->
-  let loc = {
-    loc_filename = file;
-    loc_line = line;
-    loc_start = st;
-    loc_end = en;
-  } in
-  { frame_location = Some loc; frame_raised = r; }
-
-let rec repr_aux accu = function
-| [] -> accu
-| fragment :: stack ->
-  let len = Array.length fragment in
-  let rec append accu i =
-    if i = len then accu
-    else append (of_raw fragment.(i) :: accu) (succ i)
-  in
-  repr_aux (append accu 0) stack
-
-let repr bt = repr_aux [] (List.rev bt)
-
-let push stack = match get_exception_backtrace () with
-| None -> []
-| Some frames -> frames :: stack
-
-(** Utilities *)
-
-let print_frame frame =
-  let raise = if frame.frame_raised then "raise" else "frame" in
-  match frame.frame_location with
-  | None -> Printf.sprintf "%s @ unknown" raise
-  | Some loc ->
-    Printf.sprintf "%s @ file \"%s\", line %d, characters %d-%d"
-      raise loc.loc_filename loc.loc_line loc.loc_start loc.loc_end
-
-(** Exception manipulation *)
-
-let backtrace : t Exninfo.t = Exninfo.make ()
-
-let is_recording = ref false
-
-let record_backtrace b =
-  let () = Printexc.record_backtrace b in
-  is_recording := b
-
-let get_backtrace e =
-  Exninfo.get e backtrace
-
-let add_backtrace e =
-  if !is_recording then
-    (* This must be the first function call, otherwise the stack may be
-       destroyed *)
-    let current = get_exception_backtrace () in
-    let info = Exninfo.info e in
-    begin match current with
-    | None -> (e, info)
-    | Some fragment ->
-      let bt = match get_backtrace info with
-      | None -> []
-      | Some bt -> bt
-      in
-      let bt = fragment :: bt in
-      (e, Exninfo.add info backtrace bt)
-    end
-  else
-    let info = Exninfo.info e in
-    (e, info)
-
-let app_backtrace ~src ~dst =
-  if !is_recording then
-    match get_backtrace src with
-    | None -> dst
-    | Some bt ->
-      match get_backtrace dst with
-      | None ->
-        Exninfo.add dst backtrace bt
-      | Some nbt ->
-        let bt = bt @ nbt in
-        Exninfo.add dst backtrace bt
-  else dst
diff --git a/clib/backtrace.mli b/clib/backtrace.mli
deleted file mode 100644
index 55c60e5483..0000000000
--- a/clib/backtrace.mli
+++ /dev/null
@@ -1,98 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** * Low-level management of OCaml backtraces.
-
-  Currently, OCaml manages its backtraces in a very imperative way. That is to
-  say, it only keeps track of the stack destroyed by the last raised exception.
-  So we have to be very careful when using this module not to do silly things.
-
-  Basically, you need to manually handle the reraising of exceptions. In order
-  to do so, each time the backtrace is lost, you must [push] the stack fragment.
-  This essentially occurs whenever a [with] handler is crossed.
-
-*)
-
-(** {5 Backtrace information} *)
-
-type location = {
-  loc_filename : string;
-  loc_line : int;
-  loc_start : int;
-  loc_end : int;
-}
-(** OCaml debugging information for function calls. *)
-
-type frame = { frame_location : location option; frame_raised : bool; }
-(** A frame contains two informations: its optional physical location, and
-    whether it raised the exception or let it pass through. *)
-
-type t
-(** Type of backtraces. They're essentially stack of frames. *)
-
-val empty : t
-(** Empty frame stack. *)
-
-val push : t -> t
-(** Add the current backtrace information to a given backtrace. *)
-
-val repr : t -> frame list
-(** Represent a backtrace as a list of frames. Leftmost element is the outermost
-    call. *)
-
-(** {5 Utilities} *)
-
-val print_frame : frame -> string
-(** Represent a frame. *)
-
-(** {5 Exception handling} *)
-
-val record_backtrace : bool -> unit
-(** Whether to activate the backtrace recording mechanism. Note that it will
-    only work whenever the program was compiled with the [debug] flag. *)
-
-val get_backtrace : Exninfo.info -> t option
-(** Retrieve the optional backtrace coming with the exception. *)
-
-val add_backtrace : exn -> Exninfo.iexn
-(** Add the current backtrace information to the given exception.
-
-    The intended use case is of the form: {[
-
-    try foo
-      with
-      | Bar -> bar
-      | err -> let err = add_backtrace err in baz
-
-    ]}
-
-    WARNING: any intermediate code between the [with] and the handler may
-    modify the backtrace. Yes, that includes [when] clauses. Ideally, what you
-    should do is something like: {[
-
-    try foo
-      with err ->
-        let err = add_backtrace err in
-        match err with
-        | Bar -> bar
-        | err -> baz
-
-    ]}
-
-    I admit that's a bit heavy, but there is not much to do...
-
-*)
-
-val app_backtrace : src:Exninfo.info -> dst:Exninfo.info -> Exninfo.info
-(** Append the backtrace from [src] to [dst]. The returned exception is [dst]
-    except for its backtrace information. This is targeted at container
-    exceptions, that is, exceptions that contain exceptions. This way, one can
-    transfer the backtrace from the container to the underlying exception, as if
-    the latter was the one originally raised. *)
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 34f76a2edd..ee998c2f17 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -57,12 +57,29 @@ let rec find_and_remove_assoc (i : int) = function
     if rem == ans then (r, l)
     else (r, (j, v) :: ans)
 
-let iraise e =
+type backtrace = Printexc.raw_backtrace
+let backtrace_to_string = Printexc.raw_backtrace_to_string
+
+let backtrace_info : backtrace t = make ()
+
+let is_recording = ref false
+
+let record_backtrace b =
+  let () = Printexc.record_backtrace b in
+  is_recording := b
+
+let get_backtrace e = get e backtrace_info
+
+let iraise (e,i) =
   let () = Mutex.lock lock in
   let id = Thread.id (Thread.self ()) in
-  let () = current := (id, e) :: remove_assoc id !current in
+  let () = current := (id, (e,i)) :: remove_assoc id !current in
   let () = Mutex.unlock lock in
-  raise (fst e)
+  match get i backtrace_info with
+  | None ->
+    raise e
+  | Some bt ->
+    Printexc.raise_with_backtrace e bt
 
 let raise ?info e = match info with
 | None ->
@@ -72,11 +89,7 @@ let raise ?info e = match info with
   let () = Mutex.unlock lock in
   raise e
 | Some i ->
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := (id, (e, i)) :: remove_assoc id !current in
-  let () = Mutex.unlock lock in
-  raise e
+  iraise (e,i)
 
 let find_and_remove () =
   let () = Mutex.lock lock in
@@ -104,3 +117,13 @@ let info e =
     (* Mismatch: the raised exception is not the one stored, either because the
        previous raise was not instrumented, or because something went wrong. *)
     Store.empty
+
+let capture e =
+  if !is_recording then
+    (* This must be the first function call, otherwise the stack may be
+       destroyed *)
+    let bt = Printexc.get_raw_backtrace () in
+    let info = info e in
+    e, add info backtrace_info bt
+  else
+    e, info e
diff --git a/clib/exninfo.mli b/clib/exninfo.mli
index 30803e3e6a..36cc44cf82 100644
--- a/clib/exninfo.mli
+++ b/clib/exninfo.mli
@@ -34,6 +34,49 @@ val get : info -> 'a t -> 'a option
 val info : exn -> info
 (** Retrieve the information of the last exception raised. *)
 
+type backtrace
+
+val get_backtrace : info -> backtrace option
+(** [get_backtrace info] does get the backtrace associated to info *)
+
+val backtrace_to_string : backtrace -> string
+(** [backtrace_to_string info] does get the backtrace associated to info *)
+
+val record_backtrace : bool -> unit
+
+val capture : exn -> iexn
+(** Add the current backtrace information to the given exception.
+
+    The intended use case is of the form: {[
+
+    try foo
+    with
+    | Bar -> bar
+    | exn ->
+      let exn = Exninfo.capture err in
+      baz
+
+    ]}
+
+    where [baz] should re-raise using [iraise] below.
+
+    WARNING: any intermediate code between the [with] and the handler may
+    modify the backtrace. Yes, that includes [when] clauses. Ideally, what you
+    should do is something like: {[
+
+    try foo
+    with exn ->
+      let exn = Exninfo.capture exn in
+      match err with
+      | Bar -> bar
+      | err -> baz
+
+    ]}
+
+    I admit that's a bit heavy, but there is not much to do...
+
+*)
+
 val iraise : iexn -> 'a
 (** Raise the given enriched exception. *)