Minor fixes to Arguments

- Implicit arguments can be mentioned anonymously:

    Arguments map {_ _} f l.

- To rename implicit arguments, the ": rename" flag must be used:

    Arguments map {T1 T2} f l : rename.

  Without the ": rename" flag arguments can be used to assert
  that a function has indeed the expected number of arguments and
  that the arguments are named as expected.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 2 insertions, 0 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2dc72f658..756f1d518 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -659,6 +659,7 @@ GEXTEND Gram
       | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
+      | IDENT "rename" -> [`Rename]
       | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
           [`ClearImplicits; `ClearScopes]
       | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4e73b3793..27de53cad 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -857,6 +857,7 @@ let rec pr_vernac = function
         | `SimplDontExposeCase -> str "simpl nomatch"
         | `SimplNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
+        | `Rename -> str "rename"
         | `ClearImplicits -> str "clear implicits"
         | `ClearScopes -> str "clear scopes")
         mods)