diff options
| author | Maxime Dénès | 2016-10-24 17:53:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-27 10:12:55 +0200 |
| commit | 6ecb796d462896a19212bcc5b8c0036833c6c85f (patch) | |
| tree | 8db7a5281797c86f8333a3c0e683b7bf6f9c0a40 | |
| parent | 5da679d276e106a62cc3368ceb7358da289ea10a (diff) | |
Proper fix for #3753 (anomaly with implicit arguments and renamings)
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
| -rw-r--r-- | library/impargs.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index a709aedeee..13816edb19 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -491,13 +491,15 @@ let implicits_of_global ref = 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.map (fun (t, il) -> t, List.map2 rename il rename_l) l + let rec rename implicits names = match implicits, names with + | [], _ -> [] + | _, [] -> implicits + | Some (_, x,y) :: implicits, Name id :: names -> + Some (id, x,y) :: rename implicits names + | imp :: implicits, _ :: names -> imp :: rename implicits names + in + List.map (fun (t, il) -> t, rename il rename_l) l with Not_found -> l - | Invalid_argument _ -> - anomaly (Pp.str "renamings list and implicits list have different lenghts") with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = |