]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/.depend
- added (hack) apply_tac_verbose (for auto)
[helm.git] / helm / ocaml / tactics / .depend
index 242671197dbba22a25c922740e9ff67ae09d7acc..6f9e704767490c24e973d394054128c9dcf381b2 100644 (file)
@@ -16,8 +16,6 @@ fourierR.cmi: proofEngineTypes.cmi
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
-proofEngineTypes.cmo: proofEngineTypes.cmi 
-proofEngineTypes.cmx: proofEngineTypes.cmi 
 newConstraints.cmo: newConstraints.cmi 
 newConstraints.cmx: newConstraints.cmi 
 match_concl.cmo: newConstraints.cmi match_concl.cmi 
@@ -44,6 +42,8 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \
 primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
     proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
     primitiveTactics.cmi 
+metadataQuery.cmo: metadataQuery.cmi 
+metadataQuery.cmx: metadataQuery.cmi 
 tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \
     primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi 
 tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \
@@ -92,5 +92,9 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \
 fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \
     proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \
     tacticals.cmx fourierR.cmi 
-statefulProofEngine.cmo: proofEngineTypes.cmi statefulProofEngine.cmi 
-statefulProofEngine.cmx: proofEngineTypes.cmx statefulProofEngine.cmi 
+history.cmo: history.cmi 
+history.cmx: history.cmi 
+statefulProofEngine.cmo: history.cmi proofEngineTypes.cmi \
+    statefulProofEngine.cmi 
+statefulProofEngine.cmx: history.cmx proofEngineTypes.cmx \
+    statefulProofEngine.cmi