]> matita.cs.unibo.it Git - helm.git/commit
- new tactic subst removes simple non recursive equalities from the context
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 29 Aug 2006 13:57:23 +0000 (13:57 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 29 Aug 2006 13:57:23 +0000 (13:57 +0000)
commit72858765956176eebbd67669db6e2cee8cdb0de0
treed2de8d7e0ef089b84dba957f68bffeffee836ac9
parent5c38b852feca23c3669b6c1cd836d6f8b8bc930a
- new tactic subst removes simple non recursive equalities from the context
- RELATIONAL updated to use the new tactic
20 files changed:
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/equalityTactics.mli
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/tacticals.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/contribs/RELATIONAL/NLE/dec.ma
helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
helm/software/matita/contribs/RELATIONAL/NLE/props.ma
helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
helm/software/matita/contribs/RELATIONAL/NPlus/props.ma
helm/software/matita/contribs/prova.ma
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactic_quickref.xml
helm/software/matita/matita.lang