From 7f1635816588ae200c8eed381d726bd29f57d899 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 27 Sep 2017 16:12:58 +0200
Subject: [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.
---
 plugins/ltac/g_ltac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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) ] ]
-- 
cgit v1.2.3