diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e0b94669c2..89ffae4b3e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -863,10 +863,14 @@ module Make | VernacNameSectionHypSet (id,set) -> return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ str ":="++spc()++pr_using set)) - | VernacRequire (exp, l) -> + | VernacRequire (from, exp, l) -> + let from = match from with + | None -> mt () + | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc () + in return ( hov 2 - (keyword "Require" ++ spc() ++ pr_require_token exp ++ + (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++ prlist_with_sep sep pr_module l) ) | VernacImport (f,l) -> |