]> matita.cs.unibo.it Git - helm.git/commit
now destruct takes an optional list of term rather than a sigle optional term
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 14 Nov 2007 20:28:58 +0000 (20:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 14 Nov 2007 20:28:58 +0000 (20:28 +0000)
commit42f2dc48b4fef5b404f406bf512d6a0cde35c067
treed711d6ed6d48b636f5f3e622ddc466e1bc2149ec
parent55891f80b4f14251dfd5c9111f22f5edcbde2e11
now destruct takes an optional list of term rather than a sigle optional term
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/destructTactic.ml
components/tactics/destructTactic.mli
components/tactics/tactics.mli