Emit a warning for void Arguments statement (Close 3713)

4 files changed, 17 insertions, 3 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2c73a974b5..0286687466 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -382,8 +382,9 @@ type vernac_expr =
       (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
       ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
-      int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes
-            | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
+      int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
+              `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
+              `DefaultImplicits ] list
   | VernacArgumentsScope of reference or_by_notation *
       scope_name option list
   | VernacReserve of simple_binder list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 17fbd85cc2..8655983c4b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -684,6 +684,7 @@ GEXTEND Gram
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
       | IDENT "rename" -> [`Rename]
+      | IDENT "assert" -> [`Assert]
       | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes]
       | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
           [`ClearImplicits; `ClearScopes]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a5235a25fa..b6ab7a2382 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -861,6 +861,7 @@ let rec pr_vernac = function
         | `ReductionNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
         | `Rename -> str "rename"
+        | `Assert -> str "assert"
         | `ExtraScopes -> str "extra scopes"
         | `ClearImplicits -> str "clear implicits"
         | `ClearScopes -> str "clear scopes")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f6bc8bbebe..d6df4b8a72 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -992,6 +992,7 @@ let vernac_declare_implicits locality r l =
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
 let vernac_declare_arguments locality r l nargs flags =
+  let assert_specified = List.mem `Assert flags in
   let extra_scope_flag = List.mem `ExtraScopes flags in
   let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
   let names, rest = List.hd names, List.tl names in
@@ -1101,12 +1102,22 @@ let vernac_declare_arguments locality r l nargs flags =
     | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
     | [] -> [] | _ :: tl -> narrow tl in
   let flags = narrow flags in
-  if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then
+  let some_simpl_flags_specified =
+    not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) in
+  if some_simpl_flags_specified then begin
     match sr with
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
          (make_section_locality locality) c (rargs, nargs, flags)
     | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+  end;
+  if not (some_renaming_specified ||
+          some_implicits_specified ||
+          some_scopes_specified ||
+          some_simpl_flags_specified) &&
+     not assert_specified then
+    msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to claer implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
+
 
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;