diff options
| author | herbelin | 2001-09-20 15:44:31 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-20 15:44:31 +0000 |
| commit | 24c0e99bbe0ad4249df41f784ff4051599dd44cd (patch) | |
| tree | 0918b5ab71fa957f425f837fd7de7342c4b4032e /contrib/xml/xmlentries.ml | |
| parent | 9c5ea6376c22187e1185e187e140d5c1765305c2 (diff) | |
Report des modifs de Claudio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlentries.ml')
| -rw-r--r-- | contrib/xml/xmlentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml index 093727f2f1..2323adaa0d 100644 --- a/contrib/xml/xmlentries.ml +++ b/contrib/xml/xmlentries.ml @@ -45,8 +45,8 @@ vinterp_add "XmlPrintAll" vinterp_add "XmlPrintModule" (function - [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printModule id None) - | [VARG_IDENTIFIER id ; VARG_STRING dn] -> + [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None) + | [VARG_QUALID id ; VARG_STRING dn] -> (fun () -> Xmlcommand.printModule id (Some dn)) | _ -> anomaly "This should be trapped");; |