From b8317dfbc4217929224d44a6e1b1bdbd9e26ce5c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Dec 2015 11:45:14 +0100
Subject: [PATCH] Remove superfluous parameter.

---
 modures/ra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/modures/ra.v b/modures/ra.v
index e6c6682da..86dde1644 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -119,7 +119,7 @@ Context `{Empty A, !RAIdentity A}.
 
 Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
 Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
-Lemma ra_unit_empty x : unit ∅ ≡ ∅.
+Lemma ra_unit_empty : unit ∅ ≡ ∅.
 Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed.
 Lemma ra_empty_least x : ∅ ≼ x.
 Proof. by exists x; rewrite (left_id _ _). Qed.
-- 
GitLab