Commit 7154d5b5 authored by Ralf Jung's avatar Ralf Jung

more failing unification places

parent 50b368c0
Pipeline #17357 passed with stage
in 17 minutes and 10 seconds
......@@ -240,7 +240,7 @@ Proof.
- by split; simpl; rewrite ?cmra_core_l.
- by split; simpl; rewrite ?cmra_core_idemp.
- intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
- assert ( n (a b1 b2 : A), b1 b2 {n} a b1 {n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
......
......@@ -165,7 +165,7 @@ Proof.
- split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
- split; simpl; [by rewrite cmra_core_idemp|done].
- intros ??; rewrite! namespace_map_included; intros [??].
by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
- intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite namespace_map_validN_eq /=.
rewrite {1}/op /cmra_op /=. case_decide; last done.
intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
......
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