From 1418f5db851acfecf12c13fb7f28642d6b1f3204 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Jan 2018 16:46:34 +0100
Subject: [PATCH] Fix wrong name.

---
 theories/proofmode/class_instances.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d6abc608c..bc070209c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -842,7 +842,7 @@ Proof.
   rewrite /ElimModal=> H. apply wand_intro_r.
   by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
 Qed.
-Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → uPred M) :
+Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → uPred M) :
   (∀ x, ElimModal P P' (Φ x) (Ψ x)) → ElimModal P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
-- 
GitLab