diff options
| author | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
| commit | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (patch) | |
| tree | cc39f942a75fd621633b1ac0999bbe4b3918fcfd /printing | |
| parent | 224d3b0e8be9b6af8194389141c9508504cf887c (diff) | |
| parent | 41e4725805588b3fffdfdc0cd5ee6859de1612b5 (diff) | |
Merge branch 'v8.5' into trunk
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) -> |