Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Joshua Yanovski
iris-coq
Commits
960ac942
Commit
960ac942
authored
Feb 13, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
rename the logic's hint DB
parent
8bc4cec0
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
8 additions
and
8 deletions
+8
-8
algebra/upred.v
algebra/upred.v
+7
-7
program_logic/viewshifts.v
program_logic/viewshifts.v
+1
-1
No files found.
algebra/upred.v
View file @
960ac942
...
...
@@ -982,12 +982,12 @@ Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End
uPred_logic
.
(
*
uPred
Hint
DB
*
)
Create
HintDb
uPred
.
Hint
Resolve
or_elim
or_intro_l
'
or_intro_r
'
:
uPred
.
Hint
Resolve
and_intro
and_elim_l
'
and_elim_r
'
:
uPred
.
Hint
Resolve
always_mono
:
uPred
.
Hint
Resolve
sep_elim_l
'
sep_elim_r
'
sep_mono
:
uPred
.
Hint
Immediate
True_intro
False_elim
:
uPred
.
(
*
Hint
DB
for
the
logic
*
)
Create
HintDb
I
.
Hint
Resolve
or_elim
or_intro_l
'
or_intro_r
'
:
I
.
Hint
Resolve
and_intro
and_elim_l
'
and_elim_r
'
:
I
.
Hint
Resolve
always_mono
:
I
.
Hint
Resolve
sep_elim_l
'
sep_elim_r
'
sep_mono
:
I
.
Hint
Immediate
True_intro
False_elim
:
I
.
End
uPred
.
program_logic/viewshifts.v
View file @
960ac942
...
...
@@ -92,7 +92,7 @@ Lemma vs_open_close N E P Q R :
Proof
.
intros
;
apply
(
always_intro
_
_
),
impl_intro_l
.
rewrite
always_and_sep_r
assoc
[(
P
★
_
)
%
I
]
comm
-
assoc
.
eapply
pvs_open_close
;
[
by
eauto
with
uPred
..
|
].
eapply
pvs_open_close
;
[
by
eauto
with
I
..
|
].
rewrite
sep_elim_r
.
apply
wand_intro_l
.
(
*
Oh
wow
,
this
is
annyoing
...
*
)
rewrite
assoc
-
always_and_sep_r
'
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment