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	9559b53134624dbee523cf6406a9852665c0ff77
tree	760855048dade8fc4b661802ea120c748c9cf74d	tree \| snapshot
parent	61caf50dcc5e8da40952178ddea0b94cd70e334a	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

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

RSS Atom

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