X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=8a9bbf667f6d86f27e1c605d426e9af09c824973;hb=17895f15479977be9b0c17d156fde4973397adb3;hp=c6201ce458e48b8e03d49924603c19f23231ef22;hpb=ae3540a0dc8b1e1cccb04b811bf558fb6fff9577;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index c6201ce45..8a9bbf667 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -56,7 +56,7 @@ type type_checked_obj = ;; exception AlreadyCooked of string;; -exception CircularDependency of string;; +exception CircularDependency of string Lazy.t;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; exception Object_not_found of UriManager.uri;; @@ -203,7 +203,6 @@ module Cache : C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t, List.map restore_in_term pl) | C.Fix (i, fl) -> - let len = List.length fl in let liftedfl = List.map (fun (name, i, ty, bo) -> @@ -212,7 +211,6 @@ module Cache : in C.Fix (i, liftedfl) | C.CoFix (i, fl) -> - let len = List.length fl in let liftedfl = List.map (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo)) @@ -356,7 +354,7 @@ module Cache : let univ = if o = None then "NO_UNIV" else "" in print_endline (su^" "^univ)) !frozen_list; - raise (CircularDependency (UriManager.string_of_uri uri)) + raise (CircularDependency (lazy (UriManager.string_of_uri uri))) end else if HT.mem cacheOfCookedObjects uri then @@ -576,7 +574,7 @@ let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri = * return the object,ugraph *) let add_trusted_uri_to_cache uri = - let o,u,_ = find_or_add_to_unchecked uri in + let _ = find_or_add_to_unchecked uri in Cache.unchecked_to_frozen uri; set_type_checking_info uri; try