X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=04b769b5c2b68366d2c1f765a39d21f7b7f43f62;hb=a21777bd2ac02fd346f168ead468405e4c300855;hp=431449e43886c6614f5e6c8b4c417e90e75fefe4;hpb=72e89daa67c3a5925e68c86d0109eceaffd1f163;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 431449e43..04b769b5c 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1665,7 +1665,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
    | (hete, hety)::tl ->
     (match (CicReduction.whd context hetype) with
         Cic.Prod (n,s,t) ->
-         if CicReduction.are_convertible context s hety then
+         if CicReduction.are_convertible context hety s then
           (CicReduction.fdebug := -1 ;
            eat_prods context (CicSubstitution.subst hete t) tl
           )