]> matita.cs.unibo.it Git - helm.git/commit
- cicInspect: relevant nodes count updated: letin nodes are not relevant
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 28 May 2009 17:17:29 +0000 (17:17 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 28 May 2009 17:17:29 +0000 (17:17 +0000)
commitd17a38ddca548c784e9efa7c55e87c80203b024d
treef95d041e982d0157f797ba3394964480c2c37a51
parentb378b7f4f2a3a897c4b69f44d4d1d54cc4d0aa56
- cicInspect: relevant nodes count updated: letin nodes are not relevant
- Procedural: reflexivity is now supported
- grafiteAst: boolean flag for include to tag inclusion of a source file. This command is relevant for .ma generation only. [ the source file of a .mma is not included in the generated .ma ]
- cicNotationLexer: unexpanded TeX macro symbols are now encoded with an extra space at the end. This is consistent with the concept of TeX sequence and fixes a bug in the renering of these symbols. The space is needed for reparsing!
19 files changed:
helm/software/components/acic_procedural/procedural2.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/acic_procedural/proceduralClassify.mli
helm/software/components/acic_procedural/proceduralTeX.ml
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/binaries/transcript/engine.ml
helm/software/components/binaries/transcript/gallina8Parser.mly
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/binaries/transcript/types.ml
helm/software/components/cic/cicInspect.ml
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/dependenciesParser.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/matita/matitacLib.ml