diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 7be0b015e..2de7945ee 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -92,14 +92,17 @@ let ids_of_named_context_avoiding avoid l = ([], avoid) (Termops.ids_of_named_context l) let combine_params avoid applied needed = - let rec aux ids app need = + let rec aux ids avoid app need = match app, need with [], need -> - let need', avoid = ids_of_named_context_avoiding avoid need in + let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in List.rev ids @ (List.map mkIdentC need'), avoid - | x :: app, _ :: need -> aux (x :: ids) app need + | _, (true, (id, _, _)) :: need -> + let id' = next_ident_away_from id avoid in + aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need + | x :: app, (false, _) :: need -> aux (x :: ids) avoid app need | _ :: _, [] -> failwith "combine_params: overly applied typeclass" - in aux [] applied needed + in aux [] avoid applied needed let compute_context_vars env l = List.fold_left (fun avoid (iid, _, c) -> @@ -123,7 +126,9 @@ let full_class_binders env l = let (id, l) = destClassApp cl in (try let c = class_info (snd id) in - let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in + let args, avoid = combine_params avoid l + (List.rev_map (fun x -> false, x) c.cl_context @ List.rev_map (fun x -> true, x) c.cl_super @ List.rev_map (fun x -> false, x) c.cl_params) + in (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid with Not_found -> unbound_class (Global.env ()) id) | Implicit -> (x :: l', avoid)) |