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 /plugins/funind | |
| 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 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |