Commit b198ab3a by Robbert Krebbers

### Remove forgotten admit in f2c246c6.

```Also, I removed the @ from lookup_weaken since the Coq bug we
experienced before somehow disappeared.```
parent e06b1653
Pipeline #2377 passed with stage
 ... @@ -123,13 +123,10 @@ Section gmap. ... @@ -123,13 +123,10 @@ Section gmap. Lemma big_sepM_proper Φ Ψ m : Lemma big_sepM_proper Φ Ψ m : (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) → ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x). ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x). Proof. (* Proof. (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives intros ?; apply (anti_symm (⊢)); apply big_sepM_mono; File "./algebra/upred_big_op.v", line 114, characters 4-131: eauto using equiv_entails, equiv_entails_sym, lookup_weaken. Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *) Qed. intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono; eauto using equiv_entails, equiv_entails_sym, @lookup_weaken. Qed. *) Admitted. Global Instance big_sepM_ne m n : Global Instance big_sepM_ne m n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!