]> matita.cs.unibo.it Git - helm.git/commit
Coercion hiding implemented. Notes:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Jul 2009 03:27:46 +0000 (03:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Jul 2009 03:27:46 +0000 (03:27 +0000)
commitc83721701dbbd44d3d547fdec6c4a5658322f424
treeedd9957bd0c473b1a3ee642ba4215980eb99a0e2
parentc3fc204cc02f1031b5d17fb0f2be1fc01e5c452f
Coercion hiding implemented. Notes:

1) hiding of coercions whose return type is a product is not done correctly,
   since the "sats" information seem to have changed semantics. Enrico, is it
   a bug or just a new semantics?
2) coercion matching has been implemented trivially (O(n)) in NCicCoercion.
   Here I need a special version of a discrimination tree. Enrico, do we have
   one already or is there a way to simulate it?
17 files changed:
helm/software/components/METAS/meta.helm-ng_cic_content.src
helm/software/components/Makefile
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/binaries/transcript/.depend
helm/software/components/extlib/discrimination_tree.ml
helm/software/components/extlib/discrimination_tree.mli
helm/software/components/extlib/hExtlib.mli
helm/software/components/ng_cic_content/nTermCicContent.ml
helm/software/components/ng_cic_content/nTermCicContent.mli
helm/software/components/ng_refiner/nCicCoercion.ml
helm/software/components/ng_refiner/nCicCoercion.mli
helm/software/matita/applyTransformation.ml
helm/software/matita/applyTransformation.mli
helm/software/matita/matita.ml
helm/software/matita/matitaGuiTypes.mli
helm/software/matita/matitaMathView.ml
helm/software/matita/nlibrary/algebra/magmas.ma