diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 5d689faa0b..4cf8e98228 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 |