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/success/RecTutorial.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/success/RecTutorial.v')

diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
 
 
 Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
 Arguments Vector.hd [A n].
 Arguments Vector.tl [A n].
 
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).
-- 
cgit v1.2.3