]> matita.cs.unibo.it Git - helm.git/commit
New modules stack:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 27 Nov 2008 17:44:31 +0000 (17:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 27 Nov 2008 17:44:31 +0000 (17:44 +0000)
commit3323758b99384afb5c7a70aa31bc006a78af64dd
treed1e24a0f9b7112900f90b624e7a52ad26ba8eb54
parentf4d41a527321e5fbdc10054b46ad60fe9f7f54a1
New modules stack:
grafiteDisambiguator | cicDisambiguator |
                                        | multiPassDisambiagutor |disambiguate
                       nCicDisambiguator|
22 files changed:
helm/software/components/METAS/meta.helm-disambiguation.src [new file with mode: 0644]
helm/software/components/METAS/meta.helm-ng_disambiguation.src
helm/software/components/cic_disambiguation/cicDisambiguate.ml
helm/software/components/cic_disambiguation/cicDisambiguate.mli
helm/software/components/disambiguation/.depend [new file with mode: 0644]
helm/software/components/disambiguation/.depend.opt [new file with mode: 0644]
helm/software/components/disambiguation/Makefile
helm/software/components/disambiguation/disambiguate.ml
helm/software/components/disambiguation/disambiguate.mli
helm/software/components/disambiguation/multiPassDisambiguator.ml [new file with mode: 0644]
helm/software/components/disambiguation/multiPassDisambiguator.mli [new file with mode: 0644]
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/multiPassDisambiguator.ml [deleted file]
helm/software/components/grafite_parser/multiPassDisambiguator.mli [deleted file]
helm/software/components/ng_disambiguation/.depend
helm/software/components/ng_disambiguation/Makefile
helm/software/components/ng_disambiguation/nCicDisambiguate.ml [new file with mode: 0644]
helm/software/components/ng_disambiguation/nCicDisambiguate.mli [new file with mode: 0644]
helm/software/components/ng_disambiguation/nDisambiguate.ml [deleted file]
helm/software/components/ng_disambiguation/nDisambiguate.mli [deleted file]
helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml [deleted file]
helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli [deleted file]