diff options
| author | Maxime Dénès | 2017-10-13 11:17:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-13 11:17:47 +0200 |
| commit | f8975f9fce08c7d43e6e57be980cfa36635969a9 (patch) | |
| tree | 6f5ea799e9ccc9e70354125a0bcd5977c1a10997 /plugins | |
| parent | 57bca928a3c0f7dc2582a4ffb8855ed668afdea2 (diff) | |
| parent | 4e016b91f59d3bb13681a53c35fbf4a979140b83 (diff) | |
Merge PR #1103: Take Suggest Proof Using outside the kernel.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d639dd0e1c..c577cb2198 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -340,7 +340,7 @@ GEXTEND Gram command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l) + Vernacexpr.VernacProof (Some (in_tac ta), l) | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> Vernacexpr.VernacProof (ta,Some l) ] ] |