diff options
| author | Pierre-Marie Pédrot | 2017-09-08 01:39:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 01:42:31 +0200 |
| commit | 9820b2c72cbf2da61cf44456334b38683799fd58 (patch) | |
| tree | 823212610fa3bf6e6d2ba73ebfa516e4799e3107 | |
| parent | bdd594093b4fb7e46a6cae0135b6630d75bae6f6 (diff) | |
Fix coq/ltac2#24: There should be a way to turn an exn into a message.
| -rw-r--r-- | src/tac2core.ml | 9 | ||||
| -rw-r--r-- | theories/Message.v | 3 |
2 files changed, 12 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 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". |