Commit 93315c9e authored by Robbert's avatar Robbert

Merge branch 'swasey/ssrfun' into 'master'

Support tighter precedence for x.1, x.2 notation.

See merge request FP/iris-coq!93
parents e6ec2867 c8e7221b
......@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-29.0") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
]
......@@ -1514,7 +1514,7 @@ Section ofe_fun_cmra.
{ intros x. specialize (Hf12 x).
destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
exists (y1,y2); eauto. }
exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
exists (λ x, (gg x).1), (λ x, (gg x).2). split_and!=> -?; naive_solver.
Qed.
Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
......
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