Commit 4e21c156 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding destruct and error message.

parent 42eb04b9
......@@ -582,7 +582,7 @@ let match_transformation_exception (e: exn) =
". These types should be equal:\n" ^ s1 ^ "\n" ^ s2)
| Args_wrapper.Arg_hyp_not_found s ->
message_zone#buffer#set_text ("Hypothesis not found during execution of " ^ s)
| _ -> message_zone#buffer#set_text "Uncatched error"
| _ -> message_zone#buffer#set_text (Pp.sprintf "Uncatched error: %a" Exn_printer.exn_printer e)
(* Callback of a transformation *)
let callback_update_tree_transform cont status =
......
......@@ -456,9 +456,7 @@ let () = register_transform_with_args_l
"induction"
(wrap_l (Tenv (Tterm (Tterm Ttrans_l))) induction)
(*
let () = register_transform_with_args_l
~desc:"destruct <name> destructs the head constructor of hypothesis name"
"destruct"
(wrap_l (Tprsymbol Ttrans_l) destruct)
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment