bumped version (tag soon)

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index f63b1618c5e6f4db654571a08ea7ddf8829cd1a8..22138dde8d1eee672f46385db7bc68f9428c29d7 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -129,7 +129,7 @@ module Cache :
              in
               C.Meta(i,l')
           | C.Sort _ as t -> t
-          | C.Implicit as t -> t
+          | C.Implicit _ as t -> t
           | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
           | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
           | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
@@ -351,7 +351,7 @@ let is_type_checked ?(trust=true) uri =
     Cache.unchecked_to_frozen uri ;
     if trust && trust_obj uri then
      begin
-      Logger.log (`Trusting uri) ;
+      CicLogger.log (`Trusting uri) ;
       set_type_checking_info uri ;
       CheckedObj (Cache.find_cooked uri)
      end