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 /pretyping/recordops.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 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 94119975a..fe3606ce4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -221,7 +221,7 @@ let open_canonical_structure i (_,o) = let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let ocs = try Some (List.assoc cs_pat l) + let ocs = try Some (List.assoc_f Pervasives.(=) cs_pat l) (* FIXME *) with Not_found -> None in match ocs with | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table; @@ -287,7 +287,7 @@ let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) let lookup_canonical_conversion (proj,pat) = - List.assoc pat (Refmap.find proj !object_table) + List.assoc_f Pervasives.(=) pat (Refmap.find proj !object_table) (* FIXME *) let is_open_canonical_projection env sigma (c,args) = try |