Skip to content

GitLab

Commit 8ff1fd84 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Improve error messages of iSplitL and iSplitR. 

This fixes issue #25.
parent 25f1b889
Hide whitespace changes
Inline Side-by-side
Showing with 4 additions and 2 deletions
proofmode/tactics.v
View file @ 8ff1fd84
......@@ -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 "".
......
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