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

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

author	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Mon, 16 Nov 2009 17:09:31 +0000 (17:09 +0000)
committer	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Mon, 16 Nov 2009 17:09:31 +0000 (17:09 +0000)
commit	2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce
tree	7901789f41a926baeddd08ebfe60fbc85689d733	tree \| snapshot
parent	c6c248e635ef35e9515ed981374ce2a0cef30e62	commit \| diff

Implementation of ndestruct tactic (including destruction of constructor forms
in the dependently typed case; not including discrimination of cycles).

62 files changed:

helm/software/components/acic_content/.depend.opt		diff \| blob \| history
helm/software/components/acic_procedural/.depend.opt		diff \| blob \| history
helm/software/components/binaries/extractor/.depend.opt		diff \| blob \| history
helm/software/components/binaries/table_creator/.depend.opt		diff \| blob \| history
helm/software/components/binaries/transcript/.depend		diff \| blob \| history
helm/software/components/binaries/transcript/.depend.opt		diff \| blob \| history
helm/software/components/cic/.depend.opt		diff \| blob \| history
helm/software/components/cic_acic/.depend.opt		diff \| blob \| history
helm/software/components/cic_disambiguation/.depend.opt		diff \| blob \| history
helm/software/components/cic_exportation/.depend.opt		diff \| blob \| history
helm/software/components/cic_proof_checking/.depend.opt		diff \| blob \| history
helm/software/components/cic_unification/.depend.opt		diff \| blob \| history
helm/software/components/content_pres/.depend.opt		diff \| blob \| history
helm/software/components/disambiguation/.depend.opt		diff \| blob \| history
helm/software/components/extlib/.depend.opt		diff \| blob \| history
helm/software/components/getter/.depend.opt		diff \| blob \| history
helm/software/components/grafite/.depend.opt		diff \| blob \| history
helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite_engine/.depend.opt		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_parser/.depend.opt		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/hgdome/.depend.opt		diff \| blob \| history
helm/software/components/hmysql/.depend.opt		diff \| blob \| history
helm/software/components/lexicon/.depend.opt		diff \| blob \| history
helm/software/components/library/.depend.opt		diff \| blob \| history
helm/software/components/logger/.depend.opt		diff \| blob \| history
helm/software/components/metadata/.depend.opt		diff \| blob \| history
helm/software/components/ng_cic_content/.depend.opt		diff \| blob \| history
helm/software/components/ng_disambiguation/.depend.opt		diff \| blob \| history
helm/software/components/ng_kernel/.depend		diff \| blob \| history
helm/software/components/ng_kernel/.depend.opt		diff \| blob \| history
helm/software/components/ng_kernel/nCicTypeChecker.mli		diff \| blob \| history
helm/software/components/ng_library/.depend		diff \| blob \| history
helm/software/components/ng_library/.depend.opt		diff \| blob \| history
helm/software/components/ng_paramodulation/.depend.opt		diff \| blob \| history
helm/software/components/ng_refiner/.depend.opt		diff \| blob \| history
helm/software/components/ng_tactics/.depend		diff \| blob \| history
helm/software/components/ng_tactics/.depend.opt		diff \| blob \| history
helm/software/components/ng_tactics/Makefile		diff \| blob \| history
helm/software/components/ng_tactics/nTacStatus.ml		diff \| blob \| history
helm/software/components/ng_tactics/nTacStatus.mli		diff \| blob \| history
helm/software/components/ng_tactics/nTactics.ml		diff \| blob \| history
helm/software/components/ng_tactics/nTactics.mli		diff \| blob \| history
helm/software/components/registry/.depend.opt		diff \| blob \| history
helm/software/components/syntax_extensions/.depend		diff \| blob \| history
helm/software/components/syntax_extensions/.depend.opt		diff \| blob \| history
helm/software/components/tactics/.depend.opt		diff \| blob \| history
helm/software/components/thread/.depend.opt		diff \| blob \| history
helm/software/components/tptp_grafite/.depend.opt		diff \| blob \| history
helm/software/components/urimanager/.depend.opt		diff \| blob \| history
helm/software/components/whelp/.depend.opt		diff \| blob \| history
helm/software/components/xml/.depend.opt		diff \| blob \| history
helm/software/components/xmldiff/.depend.opt		diff \| blob \| history
helm/software/matita/.depend		diff \| blob \| history
helm/software/matita/contribs/POPLmark/depends		diff \| blob \| history
helm/software/matita/matita.lang		diff \| blob \| history
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/logic/pts.ma		diff \| blob \| history
helm/software/matita/tests/destruct_bb.ma		diff \| blob \| history

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

RSS Atom