diff options
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) ] ] |