diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-08 14:25:51 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-08 14:25:51 +0000 |
| commit | 4647a3da9a617220f777f3f272a5dc20a618bd72 (patch) | |
| tree | dd023cc665d445c87e0527756d25ae550055ebbe /contrib/xml | |
| parent | 5931c481426ab253473c7539656c0f6bb50c662c (diff) | |
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
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 7faf74db8..46165871a 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -244,12 +244,13 @@ let double_type_of env sigma cstr expectedty subterms_to_types = None -> (* No expected type *) {synthesized = synthesized' ; expected = None}, synthesized - (*CSC: in HELM we did not considered Casts to be irrelevant. *) - (*CSC: does it really matter? (eq_constr is up to casts) *) | Some ty when Term.eq_constr synthesized' ty -> - (* The expected type is synthactically equal to *) - (* the synthesized type. Let's forget it. *) - {synthesized = synthesized' ; expected = None}, synthesized + (* The expected type is synthactically equal to the *) + (* synthesized type. Let's forget it. *) + (* Note: since eq_constr is up to casts, it is better *) + (* to keep the expected type, since it can bears casts *) + (* that change the innersort to CProp *) + {synthesized = ty ; expected = None}, ty | Some expectedty' -> {synthesized = synthesized' ; expected = Some expectedty'}, expectedty' |