Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
134e121d
Commit
134e121d
authored
Nov 16, 2016
by
Robbert Krebbers
Browse files
Replace deprecated appcontext > context.
parent
2a7755fe
Changes
2
Hide whitespace changes
Inline
Sidebyside
prelude/option.v
View file @
134e121d
...
@@ 298,11 +298,11 @@ End union_intersection_difference.
...
@@ 298,11 +298,11 @@ End union_intersection_difference.
(** * Tactics *)
(** * Tactics *)
Tactic
Notation
"case_option_guard"
"as"
ident
(
Hx
)
:
=
Tactic
Notation
"case_option_guard"
"as"
ident
(
Hx
)
:
=
match
goal
with
match
goal
with

H
:
app
context
C
[@
mguard
option
_
?P
?dec
]

_
=>

H
:
context
C
[@
mguard
option
_
?P
?dec
]

_
=>
change
(@
mguard
option
_
P
dec
)
with
(
λ
A
(
f
:
P
→
option
A
),
change
(@
mguard
option
_
P
dec
)
with
(
λ
A
(
f
:
P
→
option
A
),
match
@
decide
P
dec
with
left
H'
=>
f
H'

_
=>
None
end
)
in
*
;
match
@
decide
P
dec
with
left
H'
=>
f
H'

_
=>
None
end
)
in
*
;
destruct_decide
(@
decide
P
dec
)
as
Hx
destruct_decide
(@
decide
P
dec
)
as
Hx


app
context
C
[@
mguard
option
_
?P
?dec
]
=>


context
C
[@
mguard
option
_
?P
?dec
]
=>
change
(@
mguard
option
_
P
dec
)
with
(
λ
A
(
f
:
P
→
option
A
),
change
(@
mguard
option
_
P
dec
)
with
(
λ
A
(
f
:
P
→
option
A
),
match
@
decide
P
dec
with
left
H'
=>
f
H'

_
=>
None
end
)
in
*
;
match
@
decide
P
dec
with
left
H'
=>
f
H'

_
=>
None
end
)
in
*
;
destruct_decide
(@
decide
P
dec
)
as
Hx
destruct_decide
(@
decide
P
dec
)
as
Hx
...
@@ 326,9 +326,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
...
@@ 326,9 +326,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
assert
(
mx
=
Some
x'
)
as
H
by
tac
assert
(
mx
=
Some
x'
)
as
H
by
tac

assert
(
mx
=
None
)
as
H
by
tac
]

assert
(
mx
=
None
)
as
H
by
tac
]
in
repeat
match
goal
with
in
repeat
match
goal
with

H
:
app
context
[@
mret
_
_
?A
]

_
=>

H
:
context
[@
mret
_
_
?A
]

_
=>
change
(@
mret
_
_
A
)
with
(@
Some
A
)
in
H
change
(@
mret
_
_
A
)
with
(@
Some
A
)
in
H


app
context
[@
mret
_
_
?A
]
=>
change
(@
mret
_
_
A
)
with
(@
Some
A
)


context
[@
mret
_
_
?A
]
=>
change
(@
mret
_
_
A
)
with
(@
Some
A
)

H
:
context
[
mbind
(
M
:
=
option
)
(
A
:
=
?A
)
?f
?mx
]

_
=>

H
:
context
[
mbind
(
M
:
=
option
)
(
A
:
=
?A
)
?f
?mx
]

_
=>
let
Hx
:
=
fresh
in
assert_Some_None
A
mx
Hx
;
rewrite
Hx
in
H
;
clear
Hx
let
Hx
:
=
fresh
in
assert_Some_None
A
mx
Hx
;
rewrite
Hx
in
H
;
clear
Hx

H
:
context
[
fmap
(
M
:
=
option
)
(
A
:
=
?A
)
?f
?mx
]

_
=>

H
:
context
[
fmap
(
M
:
=
option
)
(
A
:
=
?A
)
?f
?mx
]

_
=>
...
...
prelude/tactics.v
View file @
134e121d
...
@@ 158,7 +158,7 @@ Coqclub message:
...
@@ 158,7 +158,7 @@ Coqclub message:
https://sympa.inria.fr/sympa/arc/coqclub/201210/msg00147.html *)
https://sympa.inria.fr/sympa/arc/coqclub/201210/msg00147.html *)
Ltac
fold_classes
:
=
Ltac
fold_classes
:
=
repeat
match
goal
with
repeat
match
goal
with


app
context
[
?F
]
=>


context
[
?F
]
=>
progress
match
type
of
F
with
progress
match
type
of
F
with

FMap
_
=>

FMap
_
=>
change
F
with
(@
fmap
_
F
)
;
change
F
with
(@
fmap
_
F
)
;
...
@@ 176,7 +176,7 @@ Ltac fold_classes :=
...
@@ 176,7 +176,7 @@ Ltac fold_classes :=
end
.
end
.
Ltac
fold_classes_hyps
H
:
=
Ltac
fold_classes_hyps
H
:
=
repeat
match
type
of
H
with
repeat
match
type
of
H
with

app
context
[
?F
]
=>

context
[
?F
]
=>
progress
match
type
of
F
with
progress
match
type
of
F
with

FMap
_
=>

FMap
_
=>
change
F
with
(@
fmap
_
F
)
in
H
;
change
F
with
(@
fmap
_
F
)
in
H
;
...
...
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