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

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

author	Andrea Berlingieri <andrea.berlingieri@studio.unibo.it>
	Wed, 13 Mar 2019 22:18:13 +0000 (23:18 +0100)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 27 Sep 2019 13:58:07 +0000 (15:58 +0200)
commit	b6ceb877c05d27705ef163488aee38e60a86886c
tree	3dec34fd45fd7004e3f7a263225f9a38c1229e6b	tree \| snapshot
parent	baa054dbb476c30576bf11b81246008a7de53462	commit \| diff

Partially restore the assume tactic

Add a type for the assume tactic in GrafiteAst

Add pretty printing code for the assume tactic

Add a parsing rule for the assume tactic in GrafiteParser

Add a call in to the assume tactic in GrafiteEngine

Add a file for the declarative tactics to the ng_tactics module

Add code for the assume tactic in Declarative

Add syntax highlight tag for the assume tactic

Add the exact_tac signature to the interface file of nTactics

33 files changed:

matita/components/content/.depend.opt		diff \| blob \| history
matita/components/content_pres/.depend.opt		diff \| blob \| history
matita/components/disambiguation/.depend.opt		diff \| blob \| history
matita/components/extlib/.depend.opt		diff \| blob \| history
matita/components/getter/.depend.opt		diff \| blob \| history
matita/components/grafite/.depend.opt		diff \| blob \| history
matita/components/grafite/grafiteAst.ml		diff \| blob \| history
matita/components/grafite/grafiteAstPp.ml		diff \| blob \| history
matita/components/grafite_engine/.depend.opt		diff \| blob \| history
matita/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
matita/components/grafite_parser/.depend.opt		diff \| blob \| history
matita/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
matita/components/library/.depend.opt		diff \| blob \| history
matita/components/logger/.depend.opt		diff \| blob \| history
matita/components/ng_cic_content/.depend.opt		diff \| blob \| history
matita/components/ng_disambiguation/.depend.opt		diff \| blob \| history
matita/components/ng_extraction/.depend.opt		diff \| blob \| history
matita/components/ng_kernel/.depend.opt		diff \| blob \| history
matita/components/ng_library/.depend.opt		diff \| blob \| history
matita/components/ng_paramodulation/.depend.opt		diff \| blob \| history
matita/components/ng_refiner/.depend.opt		diff \| blob \| history
matita/components/ng_tactics/.depend.opt		diff \| blob \| history
matita/components/ng_tactics/Makefile		diff \| blob \| history
matita/components/ng_tactics/declarative.ml	[new file with mode: 0644]	blob
matita/components/ng_tactics/declarative.mli	[new file with mode: 0644]	blob
matita/components/ng_tactics/nTactics.mli		diff \| blob \| history
matita/components/registry/.depend.opt		diff \| blob \| history
matita/components/syntax_extensions/.depend		diff \| blob \| history
matita/components/syntax_extensions/.depend.opt		diff \| blob \| history
matita/components/thread/.depend.opt		diff \| blob \| history
matita/components/xml/.depend.opt		diff \| blob \| history
matita/matita/.depend.opt		diff \| blob \| history
matita/matita/matita.lang		diff \| blob \| history

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

RSS Atom