X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ca76827068c7b893326369800910c27676ebf1e0;hb=5f7dd050c5797ef12608feb26259d2dd9ef4bb38;hp=00e40dfa6b237a63ac3a047f2c3dcbde3acd988f;hpb=cbb7f68d7d012f385e74d466f0bce7881d9eb71c;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 00e40dfa6..ca7682706 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1350,6 +1350,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+(* FG: DEBUG ONLY   
+   prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+   prerr_endline ("TC: term   :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)   
    match t with
       C.Rel n ->
        (try
@@ -1442,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