]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed in LetIn: the cumulativity test was performed switching the order
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Oct 2008 15:55:36 +0000 (15:55 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Oct 2008 15:55:36 +0000 (15:55 +0000)
of the arguments!

helm/software/components/cic_proof_checking/cicTypeChecker.ml

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