Renamig support added to "Arguments"

Example:
  Arguments eq_refl {B y}, [B] y.
  Check (eq_refl (B := nat)).

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

1 files changed, 11 insertions, 1 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 5d689faa0..4cf8e9822 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -457,7 +457,17 @@ type implicit_discharge_request =
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global ref =
-  try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]]
+  try
+    let l = Refmap.find ref !implicits_table in
+    try
+      let rename_l = Arguments_renaming.arguments_names ref in
+      let rename imp name = match imp, name with
+       | Some (_, x,y), Name id -> Some (id, x,y)
+       | _ -> 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"
+  with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
   implicits_table := Refmap.add ref imps !implicits_table