X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=c38c15b931cdea943fda830e4097790503ef5501;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=30a886a2b47ad81acf62681117c04ce22e35b1c6;hpb=d2d20cd33c42d0897765387042c3779109bbf4fd;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 30a886a2b..c38c15b93 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 
@@ -2087,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 *)
@@ -2100,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
 ;;