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.
---
 API/API.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 04c69b025f..879323a37d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4914,7 +4914,6 @@ module G_proofs :
 sig
 
   val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
-  val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
 
 end
 
-- 
cgit v1.2.3