Library Mtac2Tests.test_escaped_var

Require Import Mtac2.Mtac2.

Require Import Bool.Bool.
Import M.notations.

Definition anat : nat.
MProof.
  _ <- M.evar nat; M.ret 0.
  Unshelve.
MQed.
Set Nested Proofs Allowed.
Definition escaped_evar : nat.
MProof.
x <- M.evar nat; M.ret x.
Unshelve.
Fail MQed. M.ret 0.
Fail MQed. Qed.