aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 220e0e050..4d8a6d5d7 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -10,8 +10,6 @@
open Names
open Term
open Vars
-open Context
-open Evd
open Environ
open Nametab
open Errors
@@ -26,7 +24,6 @@ open Constrexpr
open Decl_kinds
open Entries
-open Misctypes
let typeclasses_db = "typeclass_instances"