Whenever an extension is used, its definitions are entered into the following index. (Thus, a newly installed but never-used extension is not indexed yet.).