aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml6
1 files changed, 1 insertions, 5 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 5419a10a8..db048bbd6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -14,10 +14,8 @@ open Nameops
open Term
open Vars
open Environ
-open Globnames
-open Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
module NamedDecl = Context.Named.Declaration
(** Generic filters *)
@@ -360,8 +358,6 @@ module EvMap = Evar.Map
module EvNames :
sig
-open Misctypes
-
type t
val empty : t