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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 29 Aug 2006 13:57:23 +0000 (13:57 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 29 Aug 2006 13:57:23 +0000 (13:57 +0000)
commit	45d71beffd253ffd767a9afbfcec5c4f44afd8a8
tree	5ab65a9bf450797130574c5dd5db6e9160456d5e	tree \| snapshot
parent	4c870bba9cc89b09b4ef933bcc1667e31df09435	commit \| diff

- new tactic subst removes simple non recursive equalities from the context
- RELATIONAL updated to use the new tactic

20 files changed:

components/grafite/grafiteAst.ml		diff \| blob \| history
components/grafite/grafiteAstPp.ml		diff \| blob \| history
components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
components/grafite_parser/grafiteParser.ml		diff \| blob \| history
components/tactics/equalityTactics.ml		diff \| blob \| history
components/tactics/equalityTactics.mli		diff \| blob \| history
components/tactics/primitiveTactics.ml		diff \| blob \| history
components/tactics/primitiveTactics.mli		diff \| blob \| history
components/tactics/tacticals.ml		diff \| blob \| history
components/tactics/tactics.mli		diff \| blob \| history
matita/contribs/RELATIONAL/NLE/dec.ma		diff \| blob \| history
matita/contribs/RELATIONAL/NLE/fwd.ma		diff \| blob \| history
matita/contribs/RELATIONAL/NLE/props.ma		diff \| blob \| history
matita/contribs/RELATIONAL/NPlus/fwd.ma		diff \| blob \| history
matita/contribs/RELATIONAL/NPlus/props.ma		diff \| blob \| history
matita/contribs/prova.ma		diff \| blob \| history
matita/help/C/sec_tactics.xml		diff \| blob \| history
matita/help/C/tactic_quickref.xml		diff \| blob \| history
matita/matita.lang		diff \| blob \| history

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