diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /parsing/g_proofs.ml4 | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r-- | parsing/g_proofs.ml4 | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e254c16..017f0ea5 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -37,12 +37,12 @@ GEXTEND Gram command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_descr None) + VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr; + l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> + VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) + | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = tactic -> ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c @@ -73,8 +73,10 @@ GEXTEND Gram | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) + | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal"))) | IDENT "Show"; IDENT "Goal"; n = string -> - VernacShow (ShowGoal (GoalId n)) + VernacShow (ShowGoal (GoalUid n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode |