Reflection « src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	Application.v	8109	log plain
-rw-r--r--	ApplicationLemmas.v	4116	log plain
-rw-r--r--	CommonSubexpressionElimination.v	10059	log plain
-rw-r--r--	Conversion.v	4641	log plain
-rw-r--r--	CountLets.v	2633	log plain
-rw-r--r--	ExprInversion.v	3649	log plain
-rw-r--r--	FilterLive.v	3011	log plain
-rw-r--r--	Inline.v	3654	log plain
-rw-r--r--	InlineInterp.v	3841	log plain
-rw-r--r--	InlineWf.v	4041	log plain
-rw-r--r--	InputSyntax.v	6062	log plain
-rw-r--r--	InterpProofs.v	3050	log plain
-rw-r--r--	InterpWf.v	3353	log plain
-rw-r--r--	InterpWfRel.v	4828	log plain
-rw-r--r--	Linearize.v	3533	log plain
-rw-r--r--	LinearizeInterp.v	3766	log plain
-rw-r--r--	LinearizeWf.v	9268	log plain
-rw-r--r--	MapInterp.v	1865	log plain
-rw-r--r--	MapInterpWf.v	2616	log plain
-rw-r--r--	MapWithInterpInfo.v	10892	log plain
d---------	Named	290	log plain
-rw-r--r--	Reify.v	13870	log plain
-rw-r--r--	Syntax.v	24776	log plain
-rw-r--r--	TestCase.v	9511	log plain
-rw-r--r--	WfInversion.v	5731	log plain
-rw-r--r--	WfProofs.v	5185	log plain
-rw-r--r--	WfReflective.v	14614	log plain
-rw-r--r--	WfReflectiveGen.v	18430	log plain
-rw-r--r--	WfRel.v	2707	log plain
d---------	Z	303	log plain