matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

projects / helm.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: ad586dd) | patch

author	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 27 Nov 2008 12:39:24 +0000 (12:39 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 27 Nov 2008 12:39:24 +0000 (12:39 +0000)
commit	f4d41a527321e5fbdc10054b46ad60fe9f7f54a1
tree	b4732a67fe475b0edc43e1c9d782d5df4964a863	tree \| snapshot
parent	ad586dd2ff1080ad6d71587a07772c2596b32a96	commit \| diff

cic_disambiguation splitted into disambiguation and cic_disambiguation

18 files changed:

helm/software/components/METAS/meta.helm-cic_disambiguation.src		diff \| blob \| history
helm/software/components/Makefile		diff \| blob \| history
helm/software/components/cic_disambiguation/.depend		diff \| blob \| history
helm/software/components/cic_disambiguation/Makefile		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguate.crit2.ml	[deleted file]	blob \| history
helm/software/components/cic_disambiguation/disambiguate.crit4.ml	[deleted file]	blob \| history
helm/software/components/cic_disambiguation/disambiguate.ml	[deleted file]	blob \| history
helm/software/components/cic_disambiguation/disambiguate.mli	[deleted file]	blob \| history
helm/software/components/cic_disambiguation/disambiguateTypes.ml	[deleted file]	blob \| history
helm/software/components/cic_disambiguation/disambiguateTypes.mli	[deleted file]	blob \| history
helm/software/components/disambiguation/Makefile	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguate.crit2.ml	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguate.crit4.ml	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguate.ml	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguate.mli	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguateTypes.ml	[new file with mode: 0644]	blob
helm/software/components/disambiguation/disambiguateTypes.mli	[new file with mode: 0644]	blob
helm/software/configure.ac		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.