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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Sat, 2 Jul 2005 14:42:46 +0000 (14:42 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Sat, 2 Jul 2005 14:42:46 +0000 (14:42 +0000)
commit	ed207660b8a0fa34f1d34b9dbb41144c5be29e68
tree	14d1c3d6952d52cb710f8dd0d7f84f7294283c05	tree \| snapshot
parent	0bf30da6d3f539145bac0213887789f87bc8cc6a	commit \| diff

All the equalityTactics have now been ported to use both the equality of
Coq and that of Matita.

Note: the only problematic tactic is replace that must pick an equality without
any hint. Right now it always picks the one of matita.

helm/ocaml/cic/.depend		diff \| blob \| history
helm/ocaml/cic/Makefile		diff \| blob \| history
helm/ocaml/cic/libraryObjects.ml	[new file with mode: 0644]	blob
helm/ocaml/cic/libraryObjects.mli	[new file with mode: 0644]	blob
helm/ocaml/cic/matitaLibraryObjects.ml	[new file with mode: 0644]	blob
helm/ocaml/cic/matitaLibraryObjects.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/equalityTactics.ml		diff \| blob \| history

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

RSS Atom