]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/.depend
Universes introduction
[helm.git] / helm / ocaml / tactics / .depend
index 683e59f8871e52ad03d7d9c47639a37314a75c9b..608260c830df489f2847f4cf1dc79d0aca331f3a 100644 (file)
@@ -16,8 +16,6 @@ proofEngineReduction.cmo: proofEngineReduction.cmi
 proofEngineReduction.cmx: proofEngineReduction.cmi 
 proofEngineHelpers.cmo: proofEngineHelpers.cmi 
 proofEngineHelpers.cmx: proofEngineHelpers.cmi 
-fourier.cmo: fourier.cmi 
-fourier.cmx: fourier.cmi 
 tacticals.cmo: proofEngineTypes.cmo tacticals.cmi 
 tacticals.cmx: proofEngineTypes.cmx tacticals.cmi 
 reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi 
@@ -70,6 +68,8 @@ ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \
 ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \
     proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \
     ring.cmi 
+fourier.cmo: fourier.cmi 
+fourier.cmx: fourier.cmi 
 fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \
     proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \
     tacticals.cmi fourierR.cmi