Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
c1d6ef7f
Commit
c1d6ef7f
authored
Aug 13, 2019
by
Robbert Krebbers
Browse files
Bump stdpp.
parent
b6d1a1d6
Pipeline
#19038
failed with stage
in 0 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
opam
View file @
c1d6ef7f
...
...
@@ -12,5 +12,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-0
7-08.0.2e0bf441
") | (= "dev") }
"coq-stdpp" { (= "dev.2019-0
8-13.1.6827b242
") | (= "dev") }
]
theories/algebra/gmap.v
View file @
c1d6ef7f
...
...
@@ -34,7 +34,7 @@ Definition gmap_compl `{Cofe A} : Compl gmapO := λ c,
Global
Program
Instance
gmap_cofe
`
{
Cofe
A
}
:
Cofe
gmapO
:
=
{|
compl
:
=
gmap_compl
|}.
Next
Obligation
.
intros
?
n
c
k
.
rewrite
/
compl
/
gmap_compl
lookup_imap
.
intros
?
n
c
k
.
rewrite
/
compl
/
gmap_compl
map_
lookup_imap
.
feed
inversion
(
λ
H
,
chain_cauchy
c
0
n
H
k
)
;
simplify_option_eq
;
auto
with
lia
.
by
rewrite
conv_compl
/=
;
apply
reflexive_eq
.
Qed
.
...
...
@@ -156,7 +156,7 @@ Proof.
last
by
rewrite
-
lookup_op
.
exists
(
map_imap
(
λ
i
_
,
projT1
(
FUN
i
))
y1
).
exists
(
map_imap
(
λ
i
_
,
proj1_sig
(
projT2
(
FUN
i
)))
y2
).
split
;
[|
split
]=>
i
;
rewrite
?lookup_op
!
lookup_imap
;
split
;
[|
split
]=>
i
;
rewrite
?lookup_op
!
map_
lookup_imap
;
destruct
(
FUN
i
)
as
(
z1i
&
z2i
&
Hmi
&
Hz1i
&
Hz2i
)=>/=.
+
destruct
(
y1
!!
i
),
(
y2
!!
i
)
;
inversion
Hz1i
;
inversion
Hz2i
;
subst
=>//.
+
revert
Hz1i
.
case
:
(
y1
!!
i
)=>[?|]
//.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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