diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 09:41:19 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 09:41:19 +0000 |
| commit | a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 (patch) | |
| tree | 02972edf2946cbb9f4a30133d9f66dd5cdbe7987 /interp/implicit_quantifiers.ml | |
| parent | bb5e6d7c39211349d460db0b61b2caf3d099d5b6 (diff) | |
Turn many List.assoc into List.assoc_f
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4b4b36865..734b330e7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -219,8 +219,9 @@ let combine_params avoid fn applied needed = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named -> - aux (List.assoc id named :: ids) avoid app need + | app, (_, (Name id, _, _)) :: need + when List.mem_assoc_f Id.equal id named -> + aux (List.assoc_f Id.equal id named :: ids) avoid app need | (x, None) :: app, (None, (Name id, _, _)) :: need -> aux (x :: ids) avoid app need |