diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 18:02:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:52:56 +0200 |
| commit | dfac5aa2285de5b89f08ada3c30c0a1594737440 (patch) | |
| tree | 37fa3f3481d03c4a777595e1ec0eab631cd528aa /parsing | |
| parent | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff) | |
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e3c4b880..6ce7ca023 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -26,6 +26,8 @@ let hint_proof_using e = function | None -> None | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) +let in_tac tac = Genarg.in_gen (Genarg.rawwit Constrarg.wit_ltac) tac + (* Proof commands *) GEXTEND Gram GLOBAL: command; @@ -41,9 +43,9 @@ GEXTEND Gram | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) + VernacProof (Some (in_tac 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 ] -> + ta = OPT [ "with"; ta = tactic -> in_tac ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None @@ -127,7 +129,7 @@ GEXTEND Gram | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> - HintsExtern (n,c,tac) ] ] + HintsExtern (n,c, in_tac tac) ] ] ; constr_body: [ [ ":="; c = lconstr -> c |