[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
...
```

1 files changed, 31 insertions, 8 deletions

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