Library Mtac2Tests.debug_ex

From Mtac2 Require Import Base Datatypes.
Import M.
Import M.notations.

Goal True.
MProof.
  Fail raise _.   Mtac Do Set_Debug_Exceptions.
  Fail raise _.   Fail nu "P" mNone (fun P:True=>M.ret P).   Fail (_:M True).   Mtac Do Unset_Debug_Exceptions.
  Fail (_:M True).   M.ret I.
Qed.