From 3c535011374382bc205a68b1cb59cfa7247d544a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 15 Dec 2015 17:46:25 +0100
Subject: Extraction: fix a few little glitches with my last commit (replacing
 unused vars by _)

---
 plugins/extraction/common.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'plugins/extraction/common.ml')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 97f856944c..8cf3b8194c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -171,10 +171,7 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let get_db_name n (db,_) =
-  let id = List.nth db (pred n) in
-  if Id.equal id dummy_name then Id.of_string "__" else id
-
+let get_db_name n (db,_) = List.nth db (pred n)
 
 (*S Renamings of global objects. *)
 
-- 
cgit v1.2.3