From dad9e782659d0c9c8b77b90b2b8e1f23ce9655de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 25 Feb 2018 12:51:26 +0100
Subject: [PATCH] Fix `Arguments` of `ElimInv`.

Thanks to @jtassaro for reporting.
---
 theories/proofmode/classes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 0bd44bb97..4fff53f23 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -501,8 +501,8 @@ Hint Mode IntoInv + ! - : typeclass_instances.
 *)
 Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
   elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
-Arguments ElimInv {_} _ _ _%I _%I _%I _%I : simpl never.
-Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I.
+Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
 Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
 
 (* We make sure that tactics that perform actions on *specific* hypotheses or
-- 
GitLab