diff options
Diffstat (limited to 'contrib/xml/xmlentries.ml4')
| -rw-r--r-- | contrib/xml/xmlentries.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index bcfcbd2ff..2807a3d6e 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -50,7 +50,7 @@ END let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt () let _ = - Pptactic.declare_extra_genarg_pprule + Pptactic.declare_extra_genarg_pprule true (rawwit_filename, pr_filename) (wit_filename, pr_filename) @@ -76,7 +76,7 @@ open Pp let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt () let _ = - Pptactic.declare_extra_genarg_pprule + Pptactic.declare_extra_genarg_pprule true (rawwit_diskname, pr_diskname) (wit_diskname, pr_diskname) |