no longer build oldDisambiguate

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

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 82b678e1e78f80a3ed0490eb9f21ca6fcd34a10f..d1cda56b31a1d331e8f58e87b65d4a722e34bed2 100644 (file)
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -7,10 +7,8 @@ proofEngine.cmo: proofEngine.cmi
 proofEngine.cmx: proofEngine.cmi 
 logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
 logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi 
-oldDisambiguate.cmo: oldDisambiguate.cmi 
-oldDisambiguate.cmx: oldDisambiguate.cmi 
-disambiguatingParser.cmo: oldDisambiguate.cmi disambiguatingParser.cmi 
-disambiguatingParser.cmx: oldDisambiguate.cmx disambiguatingParser.cmi 
+disambiguatingParser.cmo: disambiguatingParser.cmi 
+disambiguatingParser.cmx: disambiguatingParser.cmi 
 termEditor.cmo: disambiguatingParser.cmi termEditor.cmi 
 termEditor.cmx: disambiguatingParser.cmx termEditor.cmi 
 texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi