diff options
| author | letouzey | 2013-10-24 09:41:19 +0000 |
|---|---|---|
| committer | letouzey | 2013-10-24 09:41:19 +0000 |
| commit | a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 (patch) | |
| tree | 02972edf2946cbb9f4a30133d9f66dd5cdbe7987 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | printing/printmod.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2b66844480..e19be4e12e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -960,7 +960,7 @@ and pr_extend s cl = try pr_gen a with Failure _ -> str ("<error in "^s^">") in try - let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in + let rls = List.assoc_f String.equal s (Egramml.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with diff --git a/printing/printmod.ml b/printing/printmod.ml index b5d1d8a181..b5f84c79e0 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 |