From 0780de3f579681aa80e5e353d3aaeeaa418f2369 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Dec 2009 12:05:57 +0000
Subject: Continuing r12485-12486 (cleaning around name generation) - backtrack
 on incompatibility introduced in intro while trying to   simplify the
 condition about when to restart the subscript of a name   (the legacy says:
 find a new name from x0 if the name xN exists in   the context but find a new
 name from xN+1 if the name xN does not   exists in the context but is a
 global to avoid). - made the names chosen by "intro" compliant with the ones
 printed in   the goal and used for "intros until" (possible source of rare  
 incompatibilities) [replaced the use of visibly_occur_id for   printing the
 goal into a call to next_name_away_in_goal] - also made the names internal to
 T in "T -> U" printed the same in   the goal as they are while printing T
 after it is introducted in the   hypotheses [non contravariant propagation of
 boolean isgoal in   detype_binder] - simplified a bit visibly_occur_id (the
 Rel and Var cases were useless as   soon as the avoid list contained the
 current env); still this function is   costly with polynomial time in the
 depth of binders - see file output/Naming.v for examples

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'pretyping/termops.ml')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4de4bde2cb..07ac5df215 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -523,6 +523,17 @@ 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] *)
 
-- 
cgit v1.2.3