Library Mtac2Tests.do

Require Import Mtac2.Base.
Import M.
Import M.notations.

Mtac Do (ret tt).

Mtac Do (print_term tt).

Mtac Do (ret _).
Fail Mtac Do _. Set Printing Universes.
Mtac Do New Exception Pum.
Check Pum.

Fail Mtac Do (raise Pum).

Mtac Do Check (_ + _).