From 2e79ed74824db4697ab1807b6210b3d4097c9fda Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 8 Jun 2016 02:35:52 +0200
Subject: proofs/proofs.mllib: no more proof_errors !

---
 proofs/proofs.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 9130a186ba..804a543605 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,7 +2,6 @@ Miscprint
 Goal
 Evar_refiner
 Proof_using
-Proof_errors
 Logic
 Refine
 Proof
-- 
cgit v1.2.3