From 8ff1fd84a69c86f035c8b9171791e6021f1aa52c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 23:47:37 +0200
Subject: [PATCH] Improve error messages of iSplitL and iSplitR.
This fixes issue #25.
---
proofmode/tactics.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 85791ec21..c3044b80f 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -381,13 +381,15 @@ Tactic Notation "iSplitL" constr(Hs) :=
eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
[let P := match goal with |- FromSep ?P _ _ => P end in
apply _ || fail "iSplitL:" P "not a separating conjunction"
- |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs "not found"| |].
+ |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs
+ "not found in the spatial context"| |].
Tactic Notation "iSplitR" constr(Hs) :=
let Hs := words Hs in
eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
[let P := match goal with |- FromSep ?P _ _ => P end in
apply _ || fail "iSplitR:" P "not a separating conjunction"
- |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].
+ |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs
+ "not found in the spatial context"| |].
Tactic Notation "iSplitL" := iSplitR "".
Tactic Notation "iSplitR" := iSplitL "".
--
GitLab