New: refinement is now used to disambiguate parsing.

[helm.git] / helm / gTopLevel / .depend

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 03c071b5cb5e60ff8dd26bc6bc4012de3421ed73..58de61edaed7c59b0a8e8fe215c0752bd13502ed 100644 (file)
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -22,9 +22,9 @@ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
     proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
     primitiveTactics.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmo 
-variousTactics.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \
+variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \
     proofEngineTypes.cmo tacticals.cmi variousTactics.cmi 
-variousTactics.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \
+variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \
     proofEngineTypes.cmx tacticals.cmx variousTactics.cmi 
 variousTactics.cmi: proofEngineTypes.cmo 
 introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \