]> matita.cs.unibo.it Git - helm.git/commit
- decompose tactic: decomposable constants are now allowed (they are unfolded)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Nov 2006 17:23:59 +0000 (17:23 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Nov 2006 17:23:59 +0000 (17:23 +0000)
commit137a822662f81efbbeac7ddc833fc9ffe252a70e
tree7f2393b5b4f18b6a91fe6a4d6e531f54e39bbe98
parentd0a1160d2bf67698ddcaa5f603f316ceb2e4bf96
- decompose tactic: decomposable constants are now allowed (they are unfolded)
- inline macro: now accepts an optional name prefix for disambiguation purposes
- transcript: now handles local objects correctly
18 files changed:
helm/software/components/binaries/transcript/.depend.opt [new file with mode: 0644]
helm/software/components/binaries/transcript/engine.ml
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/binaries/transcript/types.ml
helm/software/components/binaries/transcript/v8Lexer.mll
helm/software/components/binaries/transcript/v8Parser.mly
helm/software/components/extlib/hExtlib.ml
helm/software/components/extlib/hExtlib.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/eliminationTactics.mli
helm/software/components/tactics/proofEngineTypes.ml
helm/software/components/tactics/tactics.mli
helm/software/components/whelp/fwdQueries.ml
helm/software/components/whelp/fwdQueries.mli