Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" [F. Guidi: "Procedural Representation of CIC Proof Terms" Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].

category	objects
sizes	files	360	characters	646465	nodes	1812003
propositions	theorems	117	lemmas	1283	total	1400
concepts	declared	54	defined	81	total	135

The source files are grouped in planes and components according to the following table. Notation files covering the whole specification are provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).

component	plane	files
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )	lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv
	stratified native validity	snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )	snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs
equivalence	decomposed extended equivalence	cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )	cpes_cpds
	context-sensitive equivalence	cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs
conversion	context-sensitive conversion	cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )	cpc_cpc
computation	evaluation for context-sensitive extended reduction	cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
	evaluation for context-sensitive reduction	cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )	cpre_cpre
	strongly normalizing "big tree" computation	fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )	fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )	fsb_aaa fsb_csx
	strongly normalizing extended computation	lcosx ( ? ⊢ ~⬊*[?,?,?] ? )	lcosx_cpx
		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )	lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )	lsx_ldrop lsx_lpx lsx_lpxs llsx_csx
		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )	csx_tstc_vector csx_aaa
		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )	csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )	csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
	"big tree" parallel computation	fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )	fpbg_lift fpbg_fleq fpbg_fpbg
		fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )	fpbc_fleq fpbc_fpbs
		fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )	fpbu_lift fpbu_lleq	fpbu_fleq
		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )	fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )	fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext
	decomposed extended computation	cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )	cpds_lift cpds_aaa cpds_cpds
	context-sensitive extended computation	lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )	lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )	cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
	context-sensitive computation	lprs ( ⦃?,?⦄ ⊢ ➡* ? )	lprs_ldrop lprs_cprs lprs_lprs
		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)	cprs_lift cprs_cprs
	local env. ref. for abstract candidates of reducibility	lsubc ( ? ⊢ ? ⫃[?] ? )	lsubc_ldrop lsubc_ldrops lsubc_lsuba
	support for abstract computation properties	acp	acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )	acp_aaa
reduction	"big tree" parallel reduction	fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )	fpb_lift fpb_aaa
	normal forms for context-sensitive extended reduction	cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )	cnx_lift cnx_crx cnx_cix
	context-sensitive extended reduction	lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )	lpx_ldrop lpx_frees	lpx_lleq lpx_aaa
		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )	cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
	irreducible forms for context-sensitive extended reduction	cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )	cix_lift
	reducible forms for context-sensitive extended reduction	crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )	crx_lift
	normal forms for context-sensitive reduction	cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )	cnr_lift cnr_crr cnr_cir
	context-sensitive reduction	lpr ( ⦃?,?⦄ ⊢ ➡ ? )	lpr_ldrop lpr_lpr
		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )	cpr_lift cpr_llpx_sn cpr_cir
	irreducible forms for context-sensitive reduction	cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )	cir_lift
	reducible forms for context-sensitive reduction	crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )	crr_lift
unfold	unfold	unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
	iterated static type assignment	lsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )	lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )	lsstas_lift lsstas_aaa lsstas_lsstas
static typing	local env. ref. for atomic arity assignment	lsuba ( ? ⊢ ? ⁝⫃ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba
	atomic arity assignment	aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )	aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_da aaa_ssta aaa_aaa
	stratified static type assignment	ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )	ssta_lift ssta_lpx_sn ssta_ssta
	local env. ref. for degree assignment	lsubd ( ? ⊢ ? ▪⫃ ? )	lsubd_da lsubd_lsubd
	degree assignment	da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )	da_lift da_da
	parameters	sh	sd
	restricted local env. ref.	lsubr ( ? ⫃ ? )	lsubr_lsubr
multiple substitution	lazy equivalence	fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )	fleq_fleq
		lleq ( ? ⋕[?,?] ? )	lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleq
	lazy pointwise extension of a relation	llpx_sn	llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
	pointwise union for local environments	llor ( ? ⩖[?,?] ? ≡ ? )	llor_alt llor_ldrop
	context-sensitive exclusion from free variables	frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )	frees_append frees_leq frees_lift
	contxt-sensitive extended multiple substitution	cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )	cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )	cpys_lift cpys_cpys
	iterated structural successor for closures	fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )	fqus_alt fqus_fqus
		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )	fqup_fqup
	iterated local env. slicing	ldrops ( ⇩*[?,?] ? ≡ ? )	ldrops_ldrop ldrops_ldrops
	generic term relocation	lifts_vector ( ⇧*[?] ? ≡ ? )	lifts_lift_vector
		lifts ( ⇧*[?] ? ≡ ? )	lifts_lift lifts_lifts
	support for generic relocation	gr2 ( @⦃?,?⦄ ≡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? ▭ ? ≡ ? )	gr2_gr2
substitution	structural successor for closures	fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )	fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
	global env. slicing	gget ( ⇩[?] ? ≡ ? )	gget_gget
	contxt-sensitive extended ordinary substitution	cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )	cpy_lift cpy_nlift cpy_cpy
	local env. ref. for extended substitution	lsuby ( ? ⊑×[?,?] ? )	lsuby_lsuby
	pointwise extension of a relation	lpx_sn	lpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn
	basic local env. slicing	ldrop ( ⇩[?,?,?] ? ≡ ? )	ldrop_append ldrop_leq ldrop_ldrop
	basic term relocation	lift_vector ( ⇧[?,?] ? ≡ ? )	lift_lift_vector
		lift ( ⇧[?,?] ? ≡ ? )	lift_neq lift_lift
grammar	equivalence for local environments	leq ( ? ≃[?,?] ? )	leq_leq
	same top term constructor	tstc ( ? ≃ ? )	tstc_tstc tstc_vector
	closures	cl_weight ( ♯{?,?,?} )	cl_restricted_weight ( ♯{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( ♯{?} )	lenv_length ( |?| )	lenv_append ( ? @@ ? )
		term	term_weight ( ♯{?} )	term_simple ( 𝐒⦃?⦄ )	term_vector
		item
	external syntax	aarity

The source files are grouped in directories, one for each component.