Added inversion principle creation for inductive predicates.

[helm.git] / helm / software / components / tactics / .depend

diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index 4769431a4a7badfa04ca1ee85870af68667d3503..10862a5b016c7bb78694e7e44ecb769072472c39 100644 (file)
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -120,12 +120,16 @@ discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
 discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
     proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
-inversion.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
-    proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \
-    inversion.cmi 
-inversion.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
-    proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \
-    inversion.cmi 
+inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    equalityTactics.cmi inversion.cmi 
+inversion.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    equalityTactics.cmx inversion.cmi 
+inversion_principle.cmo: tacticals.cmi proofEngineTypes.cmi \
+    primitiveTactics.cmi inversion.cmi inversion_principle.cmi 
+inversion_principle.cmx: tacticals.cmx proofEngineTypes.cmx \
+    primitiveTactics.cmx inversion.cmx inversion_principle.cmi 
 ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \
     primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi 
 ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \