diff options
| author | Enrico Tassi | 2014-12-18 16:35:46 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-18 17:08:07 +0100 |
| commit | b49d803286ba9ed711313702bb4269c5e9c516fa (patch) | |
| tree | 1f0c6407edb61f112c0872377ba2cef34386d554 /printing | |
| parent | fc3b70a11aff48eedd7b235f5732cd170a6ab8be (diff) | |
Proof using: New vernacular to name sets of section variables
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index eca67ad86a..993f9fd911 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -855,6 +855,9 @@ module Make return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id)) | VernacEndSegment id -> return (hov 2 (keyword "End" ++ spc() ++ pr_lident id)) + | VernacNameSectionHypSet (id,set) -> + return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ + str ":="++spc()++pr_using set)) | VernacRequire (exp, l) -> return ( hov 2 @@ -1208,12 +1211,14 @@ module Make | VernacProof (None, None) -> return (keyword "Proof") | VernacProof (None, Some e) -> - return (keyword "Proof " ++ pr_using e) + return (keyword "Proof " ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) | VernacProof (Some te, Some e) -> return ( - keyword "Proof" ++ spc () ++ pr_using e ++ spc() ++ + keyword "Proof" ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e ++ spc() ++ keyword "with" ++ spc() ++pr_raw_tactic te ) | VernacProofMode s -> |