The code used to compare the synthesized and the expected type (if available)

to decide whether a conversion should be generated (exporting both types).
The comparison function used is Coq alpha conversion, that is also up to
Casts. When it was successful, the only type that was kept was the synthesized
one.

In several CoRN theorems it happened that the expected type carried a few
casts to make subterms of it be of type/sort CProp (instead of Type).
These casts were forgot, and the innersort computed was imprecise.
This partial fix consists in keeping the expected type. However, it may
happen (at least in theory) that the casts to CProp are part of the
synthesized type and not of the expected type. In this case they will be
lost anyway. Properly fixing the problem would mean recur over the two
alpha-convertible terms to add the casts from both sources. However, this
operation is very expensive and I would prefer to avoid it.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6081 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions