Tactics « Util « src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	BreakMatch.v	4948	log plain
-rw-r--r--	CPSId.v	2140	log plain
-rw-r--r--	CacheTerm.v	2573	log plain
-rw-r--r--	ChangeInAll.v	353	log plain
-rw-r--r--	ClearAll.v	103	log plain
-rw-r--r--	ClearDuplicates.v	194	log plain
-rw-r--r--	ClearbodyAll.v	103	log plain
-rw-r--r--	ConstrFail.v	487	log plain
-rw-r--r--	Contains.v	283	log plain
-rw-r--r--	ConvoyDestruct.v	1085	log plain
-rw-r--r--	DebugPrint.v	2615	log plain
-rw-r--r--	DestructHead.v	4554	log plain
-rw-r--r--	DestructHyps.v	1867	log plain
-rw-r--r--	DestructTrivial.v	204	log plain
-rw-r--r--	DoWithHyp.v	602	log plain
-rw-r--r--	ESpecialize.v	132	log plain
-rw-r--r--	ETransitivity.v	948	log plain
-rw-r--r--	EvarExists.v	181	log plain
-rw-r--r--	Forward.v	812	log plain
-rw-r--r--	GetGoal.v	51	log plain
-rw-r--r--	HasBody.v	102	log plain
-rw-r--r--	Head.v	233	log plain
-rw-r--r--	HeadUnderBinders.v	826	log plain
-rw-r--r--	MoveLetIn.v	2365	log plain
-rw-r--r--	NormalizeCommutativeIdentifier.v	681	log plain
-rw-r--r--	Not.v	240	log plain
-rw-r--r--	OnSubterms.v	226	log plain
-rw-r--r--	PoseTermWithName.v	297	log plain
-rw-r--r--	PrintContext.v	420	log plain
-rw-r--r--	Revert.v	359	log plain
-rw-r--r--	RewriteHyp.v	7441	log plain
-rw-r--r--	RunTacticAsConstr.v	749	log plain
-rw-r--r--	SetEvars.v	136	log plain
-rw-r--r--	SetoidSubst.v	928	log plain
-rw-r--r--	SideConditionsBeforeToAfter.v	799	log plain
-rw-r--r--	SimplifyProjections.v	1440	log plain
-rw-r--r--	SimplifyRepeatedIfs.v	688	log plain
-rw-r--r--	SpecializeAllWays.v	247	log plain
-rw-r--r--	SpecializeBy.v	1369	log plain
-rw-r--r--	SplitInContext.v	1635	log plain
-rw-r--r--	SubstEvars.v	109	log plain
-rw-r--r--	SubstLet.v	71	log plain
-rw-r--r--	Test.v	223	log plain
-rw-r--r--	TransparentAssert.v	759	log plain
-rw-r--r--	UnfoldArg.v	628	log plain
-rw-r--r--	UnifyAbstractReflexivity.v	2266	log plain
-rw-r--r--	UniquePose.v	1010	log plain
-rw-r--r--	VM.v	1298	log plain