diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /parsing | |
| parent | dc8f9bb9033702dc7552450c5a3891fd060ee001 (diff) | |
Proof using ...
New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.
It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |