diff options
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 a36d4ae97a..e6f792054d 100644 --- a/contrib/xml/xmlentries.ml +++ b/contrib/xml/xmlentries.ml @@ -17,9 +17,9 @@ open Vernacinterp;; vinterp_add "Print" (function - [VARG_IDENTIFIER id] -> + [VARG_QUALID id] -> (fun () -> Xmlcommand.print id None) - | [VARG_IDENTIFIER id ; VARG_STRING fn] -> + | [VARG_QUALID id ; VARG_STRING fn] -> (fun () -> Xmlcommand.print id (Some fn)) | _ -> anomaly "This should be trapped");; |