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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Sun, 14 May 2006 13:53:37 +0000 (13:53 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Sun, 14 May 2006 13:53:37 +0000 (13:53 +0000)
commit	5b911ecf8bcb1644b82316d5f2709ae253a6a36d
tree	967d2420cda638f37f79a2f35a0c90a3db13dc27	tree \| snapshot
parent	9b8ad1220893070c9a98500f99355bba7775743d	commit \| diff

- Removed old proofs
- Equality.ml splittend in to subst.ml and equality.ml, the former only for substs
- patch to kill passive generated from an active that is dropped
- fixed deep subsumption

helm/software/components/tactics/.depend		diff \| blob \| history
helm/software/components/tactics/Makefile		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/inference.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/inference.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/subst.ml	[new file with mode: 0644]	blob
helm/software/components/tactics/paramodulation/subst.mli	[new file with mode: 0644]	blob

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

RSS Atom