* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
let string_of_sort = function
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 ->