diff options
| author | Emilio Jesus Gallego Arias | 2017-09-27 16:12:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-10-10 23:50:25 +0200 |
| commit | 7f1635816588ae200c8eed381d726bd29f57d899 (patch) | |
| tree | 305b8576ee8387385b80ef4ca07491739490aa38 /plugins | |
| parent | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (diff) | |
[vernac] Remove "Proof using" hacks from parser.
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
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) ] ] |