diff options
| author | herbelin | 2009-12-02 21:41:06 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-02 21:41:06 +0000 |
| commit | 4320ed3197791eda5dc29649c51dfa7f4e477c6b (patch) | |
| tree | 36d809e06ee84a797aec7c30db37e548dac36509 /pretyping | |
| parent | 3cb4411089c18351d57685f9abe455d3f61f308f (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 3 | ||||
| -rw-r--r-- | pretyping/termops.ml | 11 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
3 files changed, 1 insertions, 14 deletions
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 *) |