From 940a6286b62a095f3d6a0f3d4851f56583a852c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 23 Aug 2016 16:55:56 +0200
Subject: Arguments: give / after last ! error detection fixed

---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f69c4fa186..f87fa8a447 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1064,7 +1064,7 @@ let vernac_declare_arguments locality r l nargs flags =
     vernac_declare_implicits locality r []
   else if some_implicits_specified || List.mem `ClearImplicits flags then
     vernac_declare_implicits locality r implicits;
-  if nargs >= 0 && nargs < List.fold_left max 0 rargs then
+  if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then
     error "The \"/\" option must be placed after the last \"!\".";
   let no_flags = List.is_empty flags in
   let rec narrow = function
-- 
cgit v1.2.3