]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicEnvironment.ml
More errors localized.
[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml
index c6201ce458e48b8e03d49924603c19f23231ef22..8a9bbf667f6d86f27e1c605d426e9af09c824973 100644 (file)
@@ -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