diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 27de53cad..e10d42b9d 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -972,9 +972,12 @@ let rec pr_vernac = function (* For extension *) | VernacExtend (s,c) -> pr_extend s c - | VernacProof (Tacexpr.TacId _) -> str "Proof" - | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te - + | VernacProof (None, None) -> str "Proof" + | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l + | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te + | VernacProof (Some te, Some l) -> + str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++ + str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) | VernacSubproof None -> str "BeginSubproof" | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i |