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. --- proofs/proofs.mllib | 1 - 1 file changed, 1 deletion(-) (limited to 'proofs/proofs.mllib') diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index eaf0c693e..058e839b4 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_using Proof_type Logic Refine -- cgit v1.2.3