X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=aa0183dad1514c05367818598267012215dcf16b;hb=e7e2a523299d807370b292b44e77f46fad1638c9;hp=4226364fce18d56f7727b270b7e862da3bb2892f;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 4226364fc..aa0183dad 100644
--- 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
@@ -100,10 +100,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: computed again and again.                               *)
       let string_of_sort t =
        match CicReduction.whd context t with 
-          C.Sort C.Prop -> "Prop"
-        | C.Sort C.Set  -> "Set"
-        | C.Sort C.Type -> "Type"
-        | _ -> assert false
+          C.Sort C.Prop  -> "Prop"
+        | C.Sort C.Set   -> "Set"
+        | C.Sort C.Type  -> "Type"
+	| C.Sort C.CProp -> "CProp"
+        | _              -> assert false
       in
        let ainnertypes,innertype,innersort,expected_available =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
@@ -212,7 +213,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'