Patch to add a debugging string to HExtlib.split_nth reverted

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ca76827068c7b893326369800910c27676ebf1e0..c38c15b931cdea943fda830e4097790503ef5501 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -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
 ;;