* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
let string_of_sort = function
if global_computeinnertypes then
D.double_type_of metasenv context t expectedty
else
- D.CicHash.empty ()
+ Cic.CicHash.create 1 (* empty table *)
in
(*
let time2 = Sys.time () in
(* *)
let {D.synthesized = synthesized; D.expected = expected} =
if computeinnertypes then
- D.CicHash.find terms_to_types tt
+ Cic.CicHash.find terms_to_types tt
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
match binding with
Some (n,Cic.Def (t,_)) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
+ Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+ (Some hid);
(binding::context),
((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
| Some (n,Cic.Decl t) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
+ Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+ (Some hid);
(binding::context),
((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
| None ->