From a6832ccfacd9c105b23a9a77dadc3202f7af26fc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Sep 2016 10:46:53 +0200
Subject: Argument : assert does fail if no arg is given (fix #4864)

---
 test-suite/output/Arguments.v     | 2 +-
 test-suite/success/simpl_tuning.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac631..bd9240476f 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
index d4191b939b..2728672f30 100644
--- a/test-suite/success/simpl_tuning.v
+++ b/test-suite/success/simpl_tuning.v
@@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
 Abort. 
 
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 
 Lemma foo : volatile = volatile.
 simpl.
-- 
cgit v1.2.3