From 1788c6be52a0c6532045c57897606bffd0173eab Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 13 Oct 2008 15:55:36 +0000 Subject: [PATCH] Bug fixed in LetIn: the cumulativity test was performed switching the order of the arguments! --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2