auto.cmi: universe.cmi proofEngineTypes.cmi
autoTactic.cmi: universe.cmi proofEngineTypes.cmi
discriminationTactics.cmi: proofEngineTypes.cmi
+substTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
primitiveTactics.cmx metadataQuery.cmx paramodulation/equality.cmx \
autoTypes.cmx auto.cmx autoTactic.cmi
discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
- proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
- introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \
- discriminationTactics.cmi
+ proofEngineTypes.cmi proofEngineStructuralRules.cmi \
+ proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \
+ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi
discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
- proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
- introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \
- discriminationTactics.cmi
+ proofEngineTypes.cmx proofEngineStructuralRules.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
+ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi
+substTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
+ proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \
+ substTactic.cmi
+substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
+ proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \
+ substTactic.cmi
inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
equalityTactics.cmi inversion.cmi