]> matita.cs.unibo.it Git - helm.git/commit
Ugly solution to the "we proved T that is equivalent to T" problem:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Apr 2006 11:17:10 +0000 (11:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Apr 2006 11:17:10 +0000 (11:17 +0000)
commit7dc9e84cd0e40d8ff6847aabe780a4196e30be36
treed163d7863d748b98599d292692b9c8722e68664d
parentdb48e1ca9a2c0db7e8101367ec98e4ff2f1c069c
Ugly solution to the "we proved T that is equivalent to T" problem:
we use pack_coercion (defined into cicRefine) inside doubleTypeInference
(that is well below in the module hierarchy :-(

This is also supposed to be quite expensive (since pack_coercion uses
the refiner and coercion packing is applied to every expected/synthesized
type).
helm/software/components/cic_acic/doubleTypeInference.ml
helm/software/components/cic_acic/doubleTypeInference.mli
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/cicRefine.mli