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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_xml.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 6e6612e9a..959dba132 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -74,7 +74,7 @@ let nmtoken (loc,a) = with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") let get_xml_attr s al = - try List.assoc s al + try List.assoc_f String.equal s al with Not_found -> error ("No attribute "^s) (* Interpreting specific attributes *) @@ -124,7 +124,7 @@ let get_xml_constructor al = (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) let get_xml_binder al = - try Name (ident_of_cdata (List.assoc "binder" al)) + try Name (ident_of_cdata (List.assoc_f String.equal "binder" al)) with Not_found -> Anonymous let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) |