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 30a886a2b47ad81acf62681117c04ce22e35b1c6..ca76827068c7b893326369800910c27676ebf1e0 100644 (file)
--- 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