From 7154d5b5441a65f7eaa4b8869f2b0fe01c2062bc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Jun 2019 15:12:00 +0200
Subject: [PATCH] more failing unification places
---
theories/algebra/auth.v | 2 +-
theories/algebra/namespace_map.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 4af018de3..1d6337816 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -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 /=;
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 94789d0f1..6285c2ab0 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -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.
--
GitLab