Properly handling internal errors from Coq.

3 files changed, 29 insertions, 3 deletions

diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a1f9debdcb..dd20de5ef5 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -92,14 +92,22 @@ let to_ident c = to_ext val_ident c
 let of_pattern c = of_ext val_pattern c
 let to_pattern c = to_ext val_pattern c
 
+let internal_err =
+  let open Names in
+  KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "Internal"))
+
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
 | LtacError (kn, c) -> ValOpn (kn, c)
-| _ -> of_ext val_exn c
+| _ -> ValOpn (internal_err, [|of_ext val_exn c|])
 
 let to_exn c = match c with
-| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
-| _ -> to_ext val_exn c
+| ValOpn (kn, c) ->
+  if Names.KerName.equal kn internal_err then
+    to_ext val_exn c.(0)
+  else
+    (LtacError (kn, c), Exninfo.null)
+| _ -> assert false
 
 let of_option f = function
 | None -> ValInt 0
diff --git a/tests/errors.v b/tests/errors.v
new file mode 100644
index 0000000000..e7beff3420
--- /dev/null
+++ b/tests/errors.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Goal True.
+Proof.
+let x := Control.plus
+  (fun () => let _ := constr:(nat -> 0) in 0)
+  (fun e => match e with Not_found => 1 | _ => 2 end) in
+match Int.equal x 2 with
+| true => ()
+| false => Control.throw Tactic_failure
+end.
+Abort.
diff --git a/theories/Init.v b/theories/Init.v
index 1591747eb4..baaf5956b2 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -46,6 +46,12 @@ Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].
 
 (** Pervasive exceptions *)
 
+Ltac2 Type err.
+(** Coq internal errors. Cannot be constructed, merely passed around. *)
+
+Ltac2 Type exn ::= [ Internal (err) ].
+(** Wrapper around the errors raised by Coq implementation. *)
+
 Ltac2 Type exn ::= [ Out_of_bounds ].
 (** Used for bound checking, e.g. with String and Array. *)