From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 13 Oct 2008 15:55:36 +0000 (+0000)
Subject: Bug fixed in LetIn: the cumulativity test was performed switching the order
X-Git-Tag: make_still_working~4691
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1788c6be52a0c6532045c57897606bffd0173eab;p=helm.git

Bug fixed in LetIn: the cumulativity test was performed switching the order
of the arguments!
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 30a886a2b..ca7682706 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1446,7 +1446,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
       let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
-       R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+       R.are_convertible ~subst ~metasenv context ty' ty ugraph1
       in 
        if not b then
         raise