From 64ceb784611e5ded0c715835a36490de1c3bb1ca Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 23:27:04 -0800
Subject: Change Implicit Arguments to Arguments in algebra

---
 mathcomp/algebra/ssrint.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/ssrint.v')

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index e6c4ca6..752be45 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -970,7 +970,7 @@ End NumMorphism.
 
 End MorphTheory.
 
-Implicit Arguments intr_inj [[R] x1 x2].
+Arguments intr_inj {R} [x1 x2].
 
 Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
   match n with
-- 
cgit v1.2.3