aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-08 02:35:52 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-08 13:13:24 +0200
commit2e79ed74824db4697ab1807b6210b3d4097c9fda (patch)
tree20b855fcf8b2de985f97486b8f0edc1e00a1f4eb /proofs
parentffba3c1cd397ecab2ad6e701a6ff693d93465744 (diff)
proofs/proofs.mllib: no more proof_errors !
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofs.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 9130a186b..804a54360 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,7 +2,6 @@ Miscprint
Goal
Evar_refiner
Proof_using
-Proof_errors
Logic
Refine
Proof