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 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/extraction/common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 8cf3b8194c..bb9e8e5f5b 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*