From a2802a0b93aa24e4340be6cb3de7fff865028189 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 19 Dec 2019 16:51:04 +0100
Subject: Fix test-suite fo non maximal implicit arguments

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index ff08bdc6bb..52cc34beb3 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse)
                      (p : pu_type from mid)
                      (qs : SequenceBase pu mid to),
               SequenceBase pu from to.
-Arguments Nil [pu cxt].
+Arguments Nil {pu cxt}.
 Arguments Cons [pu from mid to].
 
 Program Fixpoint insertBase {pu : PatchUniverse}
-- 
cgit v1.2.3