From 61e71c17ec336f868747e4cd755f666b21cc0d0f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 22 Jan 2018 18:14:59 +0100
Subject: [PATCH] Fix error message.
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dfbb381f8..e8dfd8dc3 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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.
--
GitLab