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 !

---
 dev/printers.mllib  | 1 -
 proofs/proofs.mllib | 1 -
 2 files changed, 2 deletions(-)

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 74b42842c3..e39b780723 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -189,7 +189,6 @@ Logic
 Refiner
 Clenv
 Evar_refiner
-Proof_errors
 Refine
 Proof
 Proof_global
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