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

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

author	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Wed, 30 Sep 2009 13:35:06 +0000 (13:35 +0000)
committer	Wilmer Ricciotti <ricciott@cs.unibo.it>
	Wed, 30 Sep 2009 13:35:06 +0000 (13:35 +0000)
commit	ddd6560f4e70ec3306d223738a441d5f1dd3eac9
tree	df4400a4bfb5dd584dc64d9af66d6fcfe159c2c1	tree \| snapshot
parent	7ca0a000878e864c92d94f77900bc2ca0ac143b9	commit \| diff

Added initial support for inversion principles in Matita NG.
Added a case_tac tactical, performing goal selection matching metavariables by
means of their associated tag.
Added tagged implicits, which are refined as tagged metavariables.

61 files changed:

helm/software/components/Makefile		diff \| blob \| history
helm/software/components/acic_content/.depend		diff \| blob \| history
helm/software/components/acic_content/cicNotationPt.ml		diff \| blob \| history
helm/software/components/acic_procedural/.depend		diff \| blob \| history
helm/software/components/binaries/extractor/.depend		diff \| blob \| history
helm/software/components/binaries/matitaprover/Makefile		diff \| blob \| history
helm/software/components/binaries/table_creator/.depend		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		diff \| blob \| history
helm/software/components/cic_acic/.depend		diff \| blob \| history
helm/software/components/cic_disambiguation/.depend		diff \| blob \| history
helm/software/components/cic_disambiguation/cicDisambiguate.ml		diff \| blob \| history
helm/software/components/cic_exportation/.depend		diff \| blob \| history
helm/software/components/cic_proof_checking/.depend		diff \| blob \| history
helm/software/components/cic_unification/.depend		diff \| blob \| history
helm/software/components/content_pres/.depend		diff \| blob \| history
helm/software/components/content_pres/content2pres.ml		diff \| blob \| history
helm/software/components/disambiguation/.depend		diff \| blob \| history
helm/software/components/extlib/.depend		diff \| blob \| history
helm/software/components/getter/.depend		diff \| blob \| history
helm/software/components/getter/http_getter_wget.ml		diff \| blob \| history
helm/software/components/grafite/.depend		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		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.mli		diff \| blob \| history
helm/software/components/grafite_parser/.depend		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/hgdome/.depend		diff \| blob \| history
helm/software/components/hmysql/.depend		diff \| blob \| history
helm/software/components/lexicon/.depend		diff \| blob \| history
helm/software/components/library/.depend		diff \| blob \| history
helm/software/components/logger/.depend		diff \| blob \| history
helm/software/components/metadata/.depend		diff \| blob \| history
helm/software/components/ng_cic_content/.depend		diff \| blob \| history
helm/software/components/ng_disambiguation/.depend		diff \| blob \| history
helm/software/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history
helm/software/components/ng_kernel/.depend		diff \| blob \| history
helm/software/components/ng_kernel/nCic.ml		diff \| blob \| history
helm/software/components/ng_kernel/nCicPp.ml		diff \| blob \| history
helm/software/components/ng_paramodulation/.depend		diff \| blob \| history
helm/software/components/ng_refiner/.depend		diff \| blob \| history
helm/software/components/ng_refiner/nCicRefiner.ml		diff \| blob \| history
helm/software/components/ng_tactics/.depend		diff \| blob \| history
helm/software/components/ng_tactics/Makefile		diff \| blob \| history
helm/software/components/ng_tactics/nInversion.ml	[new file with mode: 0644]	blob
helm/software/components/ng_tactics/nInversion.mli	[new file with mode: 0644]	blob
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		diff \| blob \| history
helm/software/components/syntax_extensions/.depend		diff \| blob \| history
helm/software/components/tactics/.depend		diff \| blob \| history
helm/software/components/tactics/tactics.mli		diff \| blob \| history
helm/software/components/thread/.depend		diff \| blob \| history
helm/software/components/tptp_grafite/.depend		diff \| blob \| history
helm/software/components/urimanager/.depend		diff \| blob \| history
helm/software/components/whelp/.depend		diff \| blob \| history
helm/software/components/xml/.depend		diff \| blob \| history
helm/software/components/xmldiff/.depend		diff \| blob \| history

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

RSS Atom