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.

---
 pretyping/glob_ops.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 080ec5ed12..6509aaac3d 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -266,11 +266,6 @@ let occur_glob_constr id =
        fold_glob_constr_with_binders g f barred acc c in
   occur false false
 
-let add_name_to_ids set na =
-  match na with
-    | Anonymous -> set
-    | Name id -> Id.Set.add id set
-
 let free_glob_vars =
   let rec vars bound vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
-- 
cgit v1.2.3