From 9820b2c72cbf2da61cf44456334b38683799fd58 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 Sep 2017 01:39:51 +0200
Subject: Fix coq/ltac2#24: There should be a way to turn an exn into a
 message.

---
 src/tac2core.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 4a35442b04..f969183dce 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -37,6 +37,7 @@ let t_constr = coq_core "constr"
 let t_pattern = coq_core "pattern"
 let t_ident = coq_core "ident"
 let t_option = coq_core "option"
+let t_exn = coq_core "exn"
 let t_reference = std_core "reference"
 
 let c_nil = coq_core "[]"
@@ -188,6 +189,14 @@ let () = define1 "message_of_ident" ident begin fun c ->
   return (Value.of_pp pp)
 end
 
+let () = define1 "message_of_exn" valexpr begin fun v ->
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let pp = Tac2print.pr_valexpr env sigma v (GTypRef (Other Core.t_exn, [])) in
+  return (Value.of_pp pp)
+end
+
+
 let () = define2 "message_concat" pp pp begin fun m1 m2 ->
   return (Value.of_pp (Pp.app m1 m2))
 end
-- 
cgit v1.2.3