]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b0612e0) | patch
- 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)
commit885b29af55a246589b6a8966d9d1438fbb8155d3
tree9127648d1a071e6e206cbe35a8ad2fc4d3cb98catree | snapshot
parentb0612e00b2a905510439d9a6e8908497c1b74c61commit | diff
- 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:
components/binaries/transcript/.depend.opt [new file with mode: 0644] blob
components/binaries/transcript/engine.ml diff | blob | history
components/binaries/transcript/grafite.ml diff | blob | history
components/binaries/transcript/types.ml diff | blob | history
components/binaries/transcript/v8Lexer.mll diff | blob | history
components/binaries/transcript/v8Parser.mly diff | blob | history
components/extlib/hExtlib.ml diff | blob | history
components/extlib/hExtlib.mli diff | blob | history
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/grafiteParser.ml diff | blob | history
components/tactics/eliminationTactics.ml diff | blob | history
components/tactics/eliminationTactics.mli diff | blob | history
components/tactics/proofEngineTypes.ml diff | blob | history
components/tactics/tactics.mli diff | blob | history
components/whelp/fwdQueries.ml diff | blob | history
components/whelp/fwdQueries.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.