]> matita.cs.unibo.it Git - helm.git/commit
many changes regarding coercions:
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Jan 2009 10:54:34 +0000 (10:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Jan 2009 10:54:34 +0000 (10:54 +0000)
commit84e6cbe962c9a534be48542c098d7bb0d90be9a1
tree78034126c69601f0f90d0e6075699d60107d0f49
parentb7aefa8f362d07bf9042f6879252345e69da07c8
many changes regarding coercions:
- new `prefer coercion foo` command to reorder the list of coercions associated with a src >-> tgt pair
- rewritten coercions undoing mechanism
- coercion composition fixed (generates more coercions)
- librarySync rewritten, procedures to generate derived lemmas (eliminators, invertion lemmas, ...) are hooks registerd by other modules that can thus live anywhere (also in tactics/ like the one for inversion)
- manual fixed to talk about the new command
- coercions graph is drawn together with a list of coercions that makes their precedence visible (and can be altered with the prefer coercion command)
- dump-moo fixed to print coercions
- removed `Coercion attribute in XML files (YOU NEED TO RECOMPILE)
52 files changed:
helm/software/components/cic/cic.ml
helm/software/components/cic/cicParser.ml
helm/software/components/cic/cicUtil.ml
helm/software/components/cic/cicUtil.mli
helm/software/components/cic_disambiguation/.depend
helm/software/components/cic_proof_checking/.depend
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/cic_unification/coercGraph.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteMarshal.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteEngine.mli
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteSync.mli
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/library/.depend
helm/software/components/library/.depend.opt
helm/software/components/library/Makefile
helm/software/components/library/cicElim.ml
helm/software/components/library/cicElim.mli
helm/software/components/library/cicFix.ml [new file with mode: 0644]
helm/software/components/library/cicFix.mli [new file with mode: 0644]
helm/software/components/library/cicRecord.ml
helm/software/components/library/cicRecord.mli
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/librarySync.ml
helm/software/components/library/librarySync.mli
helm/software/components/library/refinementTool.ml [deleted file]
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/fourierR.ml
helm/software/components/tactics/inversion_principle.ml
helm/software/components/tactics/inversion_principle.mli
helm/software/matita/.depend
helm/software/matita/applyTransformation.ml
helm/software/matita/contribs/formal_topology/overlap/categories.ma
helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
helm/software/matita/dist/ChangeLog
helm/software/matita/dump_moo.ml
helm/software/matita/help/C/sec_commands.xml
helm/software/matita/matita.lang
helm/software/matita/matita.ml
helm/software/matita/matitaInit.ml
helm/software/matita/matitacLib.ml