Commit 61e71c17 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix error message.

parent b1f4ea08
......@@ -623,7 +623,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let e' := eval unfold e in e in clear e; go (t e')
| _ =>
let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
[apply _ || fail "iPoseProof: not a uPred"|exact t]
[apply _ || fail "iPoseProof: not a BI assertion"|exact t]
end in
go t.
......
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