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
(*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 *)
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'