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

1 files changed, 2 insertions, 1 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 4cf8e98228..badb69cb1e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -466,7 +466,8 @@ let implicits_of_global ref =
        | _ -> imp in
       List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
     with Not_found -> l
-    | Invalid_argument _ -> anomaly "renaming implicits"
+    | Invalid_argument _ ->
+        anomaly "renamings list and implicits list have different lenghts"
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =