From 72e3d2e563e08627559065ff0289403591d99682 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Aug 2017 23:49:21 +0200
Subject: Properly handling internal errors from Coq.

---
 src/tac2ffi.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3