From b92a75d3fb7ca7812d3aea4623aaa70b4de7dbb6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 15:33:01 +0200
Subject: [PATCH] Remove superfluous space in error of iPvs.
---
proofmode/pviewshifts.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 4151360ef..12ed0cd38 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -106,7 +106,7 @@ Tactic Notation "iPvsCore" constr(H) :=
eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _;
[env_cbv; reflexivity || fail "iPvs:" H "not found"
|let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
- apply _ || fail "iPvs: " P "not a pvs"
+ apply _ || fail "iPvs:" P "not a pvs"
|env_cbv; reflexivity|simpl]
end.
--
GitLab