]> matita.cs.unibo.it Git - helm.git/commit - helm/matita/matitaEngine.ml
Big commit to let Ferruccio try the merge_coercion patch.
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 7 Dec 2005 15:42:37 +0000 (15:42 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 7 Dec 2005 15:42:37 +0000 (15:42 +0000)
commit41be5e85a1103a5b14495bb487995a6a88e79c48
treed510687ab481241994f362be688e978cc0b91423
parent4dd2d3dc8e1dbb22d71c8fa741a20fb7d506930a
Big commit to let Ferruccio try the merge_coercion patch.

1) allowed :> syntax in record to specify that a field is a coercion
   (and it will be used (if needed) in defining the following projections)
2) minor cleanup in CicUtil.is_metaclosed
3) added library_objects.reset_defaults() (used in MatitaSync.init())
4) added MatitaSync.init() that is the only way to obtain an initial matita    status
5) CoercDb is only accessed by CoercGraph
6) insert_coercion flag added to the refiner (and removed the use_coercion flag    from CoercDb). Coercions are always available, the refiner will eventually    insert them
7) CicRefiner now packs coercions with the avoid_double_coercion function
8) GrafiteAstPp is now "more" in sync and dump_moo seems to work again
9) LibrarySync has a merge_coercions function that calls on
   `Generated && not(is_coercion) objects. I hope it is enough (calling it
   on every objects shlows down a bit
10)MatitaScript now calls MatitaSync.init() on reset

TODO: - remove CoercGraph.remove_coercion from add_single_obj
      - find a place for CoercGraph.add_coercion used in generate_projections
14 files changed:
helm/matita/.depend
helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
helm/matita/matita.ml
helm/matita/matitaEngine.ml
helm/matita/matitaEngine.mli
helm/matita/matitaExcPp.ml
helm/matita/matitaGui.ml
helm/matita/matitaScript.ml
helm/matita/matitaScript.mli
helm/matita/matitacLib.ml
helm/matita/matitadep.ml
helm/matita/template_makefile.in
helm/matita/tests/coercions.ma