]> matita.cs.unibo.it Git - helm.git/commit
- matitacLib: better handling of the callbacks for the dump operation
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 25 Apr 2009 13:16:47 +0000 (13:16 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 25 Apr 2009 13:16:47 +0000 (13:16 +0000)
commit6cc401c4136bafb6515bd39d86db6b5a917318bf
tree18a6039500a0226a5004da07da44c628a1d604b7
parente085135177f7b3b74b410d47a4f3bca1784b60b1
- matitacLib: better handling of the callbacks for the dump operation
- applyTransformation: notation disabled when rendering reconstructed inductive types to avoid notation conflict between notation and inductive type syntax
- lexicon/lexiconEngine: better error messages and one callback removed
- termAcicContent: in lookup_interpretations, sorting the returned interpretations is optional and defaults to true (as before)
- disambiguateChoices: in lookup_symbol_by_dsc, the interpretations are not sorted before choosing, sorting them here is a bug because their order is lost so the chosen one is not the most recent
- grafiteParser: better callback functions for the drop feature of matitac, we introduced module name abbreviations for our convenience
- syntax_extensions/.depend: something is wrong with the Makefiles, this .depend is commited every time :(
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/acic_content/termAcicContent.mli
helm/software/components/cic_disambiguation/disambiguateChoices.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/grafite_parser/grafiteParser.mli
helm/software/components/lexicon/lexiconEngine.ml
helm/software/components/lexicon/lexiconEngine.mli
helm/software/components/syntax_extensions/.depend
helm/software/matita/applyTransformation.ml
helm/software/matita/matitacLib.ml