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 +++++++++
 theories/Message.v | 3 +++
 2 files changed, 12 insertions(+)

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
diff --git a/theories/Message.v b/theories/Message.v
index 45f4b221db..7bffe0746b 100644
--- a/theories/Message.v
+++ b/theories/Message.v
@@ -19,4 +19,7 @@ Ltac2 @ external of_ident : ident -> message := "ltac2" "message_of_ident".
 Ltac2 @ external of_constr : constr -> message := "ltac2" "message_of_constr".
 (** Panics if there is more than one goal under focus. *)
 
+Ltac2 @ external of_exn : exn -> message := "ltac2" "message_of_exn".
+(** Panics if there is more than one goal under focus. *)
+
 Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat".
-- 
cgit v1.2.3