]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_disambiguation/.depend
Change Sort.merge (deprecated) with List.merge
[helm.git] / matita / components / ng_disambiguation / .depend
1 nnumber_notation.cmi :
2 disambiguateChoices.cmi :
3 nCicDisambiguate.cmi :
4 grafiteDisambiguate.cmi :
5 nnumber_notation.cmo : nnumber_notation.cmi
6 nnumber_notation.cmx : nnumber_notation.cmi
7 disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
8 disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
9 nCicDisambiguate.cmo : nCicDisambiguate.cmi
10 nCicDisambiguate.cmx : nCicDisambiguate.cmi
11 grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \
12     grafiteDisambiguate.cmi
13 grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
14     grafiteDisambiguate.cmi