Fix coq/ltac2#24: There should be a way to turn an exn into a message.

1 files changed, 9 insertions, 0 deletions

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