]> 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)
commit1ca749a387695a5a4abc138a06de496a63abac4a
tree03d0cf25634f8c4834198221e21f384d82de5b39
parent8de247e8d14940d9f619b6d35107cc5fae11b412
now destruct takes an optional list of term rather than a sigle optional term
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/destructTactic.ml
helm/software/components/tactics/destructTactic.mli
helm/software/components/tactics/tactics.mli