X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=c38c15b931cdea943fda830e4097790503ef5501;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;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..c38c15b93 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 
@@ -2083,12 +2087,12 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
    check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
 ;;
 
-let typecheck uri =
+let typecheck ?(trust=true) uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
-   match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
    | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
       (* let's typecheck the uncooked object *)
@@ -2096,7 +2100,7 @@ let typecheck uri =
       let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
       CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
       logger#log (`Type_checking_completed uri);
-      match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+      match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
       | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | _ -> raise CicEnvironmentError
 ;;