diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 9 |
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 |