From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 pretyping/typeclasses.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 817d6878..18e83056 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Context
 open Evd
-open Environ
 open Util
 open Typeclasses_errors
 open Libobject
@@ -427,7 +426,6 @@ let add_class cl =
   cl.cl_projs
 
 
-open Declarations
       
 (*
  * interface functions
@@ -485,15 +483,6 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg = function
-| Evar_kinds.GoalEvar -> false
-| _ -> true
-  (* match k with *)
-  (*     ImplicitArg (ref, (n, id), b) -> true *)
-  (*   | InternalHole -> true *)
-  (*   | _ -> false *)
-
-
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to
    goals and do not need to be resolved when we have nested [resolve_all_evars]
-- 
cgit v1.2.3