From fc2bc9f806ad7627ca2288ae9dfd27512462a5fa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 22 Dec 2018 00:42:07 +0100
Subject: Make `Add Morphism` not rely on Refine Instance

---
 test-suite/bugs/closed/bug_4498.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 379e46b3e3..9b3210860c 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -19,6 +19,6 @@ Class Category := {
 
 Require Export Coq.Setoids.Setoid.
 
-Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
-- 
cgit v1.2.3