diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e9e335ec..89ffae4b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -740,9 +740,14 @@ module Make | VernacEndProof (Proved (opac,o)) -> return ( match o with - | None -> if opac then keyword "Qed" else keyword "Defined" + | None -> (match opac with + | Transparent -> keyword "Defined" + | Opaque None -> keyword "Qed" + | Opaque (Some l) -> + keyword "Qed" ++ spc() ++ str"export" ++ + prlist_with_sep (fun () -> str", ") pr_lident l) | Some (id,th) -> (match th with - | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) ) | VernacExactProof c -> @@ -858,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) -> |