From 4320ed3197791eda5dc29649c51dfa7f4e477c6b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 2 Dec 2009 21:41:06 +0000
Subject: Continuing r12485-12486 and r12549 (cleaning around name generation)
 - fixed misunderstanding of the role of nenv while simplifying code of  
 occur_id in namegen.ml, - documented the possible incompatibilites in CHANGES
 - fixed output/Naming.v test, and fixed the count of misc. tests in  
 test-suite/check.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/recdef.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c910c4247..e153bebf4b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,8 +51,7 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  let ids = collect_visible_vars c in
-  rename_bound_vars_as_displayed ids (pf_type_of gls c)
+  rename_bound_vars_as_displayed [] (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
-- 
cgit v1.2.3