Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 4226364fce18d56f7727b270b7e862da3bb2892f..d934e83bfa4443581c161f53ef5a5d1f80f9d79e 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -37,7 +37,7 @@ let type_of_aux'_add_time = ref 0.0;;
 
 let xxx_type_of_aux' m c t =
  let t1 = Sys.time () in
- let res = TypeInference.type_of_aux' m c t in
+ let res = CicTypeChecker.type_of_aux' m c t in
  let t2 = Sys.time () in
  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
  res
@@ -212,7 +212,7 @@ Cic.Sort Cic.Type ;
                match n with
                   C.Anonymous -> n
                 | C.Name n' ->
-                   if TypeInference.does_not_occur 1 t then
+                   if DoubleTypeInference.does_not_occur 1 t then
                     C.Anonymous
                    else
                     C.Name n'