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
---
 pretyping/clenv.ml    |  3 +--
 pretyping/termops.ml  | 11 -----------
 pretyping/termops.mli |  1 -
 3 files changed, 1 insertion(+), 14 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index aa58a08082..a65cc24ff6 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -147,8 +147,7 @@ let mk_clenv_from_n gls n (c,cty) =
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
 let mk_clenv_rename_from_n gls n (c,t) =
-  let ids = collect_visible_vars t in
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed ids t)
+  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
 
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 07ac5df215..4de4bde2cb 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -523,17 +523,6 @@ let collect_metas c =
   in
   List.rev (collrec [] c)
 
-(* collects all visible var occurences (does not include indirect
-   dependencies of section variables via global references) *)
-
-let collect_visible_vars c =
-  let rec collrec acc c =
-    match kind_of_term c with
-    | Var id -> list_add_set id acc
-    | _      -> fold_constr collrec acc c
-  in
-  List.rev (collrec [] c)
-
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 44a96b613c..59f7750d3f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -109,7 +109,6 @@ val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val collect_metas : constr -> int list
-val collect_visible_vars : constr -> identifier list
 val occur_term : constr -> constr -> bool (* Synonymous
  of dependent *)
 (* Substitution of metavariables *)
-- 
cgit v1.2.3