From 777f0ace3d2458cbe1840dcf3d8f350452721e84 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Feb 2015 09:30:53 +0100 Subject: Removing dead code. --- pretyping/typeclasses_errors.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/typeclasses_errors.mli') diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index dd8087713f..7982fc8524 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -10,7 +10,6 @@ open Loc open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames -- cgit v1.2.3