let xxx_type_of_aux' m c t =
let t1 = Sys.time () in
- let res = CicTypeChecker.type_of_aux' m c t in
+ let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
let t2 = Sys.time () in
type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
res
in
let aobj =
match obj with
- C.Constant (id,Some bo,ty,params) ->
+ C.Constant (id,Some bo,ty,params,attrs) ->
let bo' = eta_fix [] [] bo in
let ty' = eta_fix [] [] ty in
let abo = acic_term_of_cic_term' bo' (Some ty') in
let aty = acic_term_of_cic_term' ty' None in
C.AConstant
- ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
- | C.Constant (id,None,ty,params) ->
+ ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
+ | C.Constant (id,None,ty,params,attrs) ->
let ty' = eta_fix [] [] ty in
let aty = acic_term_of_cic_term' ty' None in
C.AConstant
- ("mettereaposto",None,id,None,aty,params)
- | C.Variable (id,bo,ty,params) ->
+ ("mettereaposto",None,id,None,aty,params,attrs)
+ | C.Variable (id,bo,ty,params,attrs) ->
let ty' = eta_fix [] [] ty in
let abo =
match bo with
in
let aty = acic_term_of_cic_term' ty' None in
C.AVariable
- ("mettereaposto",id,abo,aty, params)
- | C.CurrentProof (id,conjectures,bo,ty,params) ->
+ ("mettereaposto",id,abo,aty,params,attrs)
+ | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
let conjectures' =
List.map
(function (i,canonical_context,term) ->
("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
*)
C.ACurrentProof
- ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
- | C.InductiveDefinition (tys,params,paramsno) ->
+ ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
+ | C.InductiveDefinition (tys,params,paramsno,attrs) ->
let context =
List.map
(fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
(id,name,inductive,acic_term_of_cic_term' ty None,acons)
) (List.rev idrefs) tys
in
- C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
+ C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
in
aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
ids_to_conjectures,ids_to_hypotheses