From e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 18:12:55 +0200
Subject: Remove dead code and unused open.

---
 interp/implicit_quantifiers.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d6749e918f..19c872b310 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -19,7 +19,6 @@ open Typeclasses_errors
 open Pp
 open Libobject
 open Nameops
-open Misctypes
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
     | [] -> bdvars, l
   in aux bound l binders
 
-let add_name_to_ids set na =
-  match na with
-  | Anonymous -> set
-  | Name id -> Id.Set.add id set
-
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
   let rec vars bound vs = function
     | GVar (loc,id) ->
-- 
cgit v1.2.3