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

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

author	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Tue, 17 Nov 2009 13:01:53 +0000 (13:01 +0000)
committer	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Tue, 17 Nov 2009 13:01:53 +0000 (13:01 +0000)
commit	2b98af47f4359ca20b42e52285c7ff4a3bd12f02
tree	bb9a7a0d09be569f8c8a0191217fffd2c1c87e21	tree \| snapshot
parent	4ae46ae1b0353b51bc77b621077fdbcd5f2d075e	commit \| diff

ndestruct tactic: mainly bugfixes; the algorithm isn't clean yet, outputting a
number of unnecessary equations which must be cleared; it seems to work
reasonably nonetheless.

helm/software/components/ng_tactics/nDestructTac.ml	[new file with mode: 0644]	blob
helm/software/components/ng_tactics/nDestructTac.mli	[new file with mode: 0644]	blob
helm/software/matita/nlibrary/logic/destruct_bb.ma		diff \| blob \| history
helm/software/matita/nlibrary/logic/equality.ma		diff \| blob \| history
helm/software/matita/nlibrary/nat/nat.ma		diff \| blob \| history

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

RSS Atom