aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 09:41:19 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 09:41:19 +0000
commita3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 (patch)
tree02972edf2946cbb9f4a30133d9f66dd5cdbe7987 /printing/printmod.ml
parentbb5e6d7c39211349d460db0b61b2caf3d099d5b6 (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 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b5d1d8a18..b5f84c79e 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -46,7 +46,7 @@ let get_new_id locals id =
get_id (List.map snd locals) id
let rec print_local_modpath locals = function
- | MPbound mbid -> pr_id (List.assoc mbid locals)
+ | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals)
| MPdot(mp,l) ->
print_local_modpath locals mp ++ str "." ++ pr_lab l
| MPfile _ -> raise Not_found