diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 11 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 9 |
2 files changed, 14 insertions, 6 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 0f5d80a83..78299448a 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -34,9 +34,15 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) - | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn + | IDENT "Proof"; "with"; ta = tactic; + l = OPT [ "using"; l = LIST0 identref -> l ] -> + VernacProof (Some ta, l) + | IDENT "Proof"; "using"; l = LIST0 identref; + ta = OPT [ "with"; ta = tactic -> ta ] -> + VernacProof (ta,Some l) + | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll | IDENT "Abort"; id = identref -> VernacAbort (Some id) @@ -56,7 +62,6 @@ GEXTEND Gram | IDENT "Resume" -> VernacResume None | IDENT "Resume"; id = identref -> VernacResume (Some id) | IDENT "Restart" -> VernacRestart - | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n 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 |