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 +-
 toplevel/vernacentries.ml         | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

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.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48a85b709f..382a716298 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -986,9 +986,9 @@ let vernac_declare_arguments locality r l nargs flags =
     | _::li, _::ld, _::ls -> check li ld ls 
     | _ -> assert false in
   let () = match l with
-  | [[]] -> ()
+  | [[]] when List.exists ((<>) `Assert) flags -> ()
   | _ ->
-    List.iter2 (fun l -> check inf_names l) (names :: rest) scopes
+    List.iter2 (check inf_names) (names :: rest) scopes
   in
   (* we take extra scopes apart, and we check they are consistent *)
   let l, scopes = 
-- 
cgit v1.2.3