| C.CurrentProof _ -> S.empty (*CSC wrong *)
| _ -> raise WrongUriToConstant
)
- | C.Abst _ -> S.empty
| C.MutInd (uri,_,_) ->
(match CicCache.get_obj uri with
C.InductiveDefinition (_, params, _) ->
let module C = Cic in
let ann = CicCache.get_annobj uri in
match ann with
- C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) ->
+ C.ADefinition (xid, id, te, ty, C.Possible pparams) ->
let te' = Deannotate.deannotate_term te in
let ty' = Deannotate.deannotate_term ty in
let real_params = parameters_of te' ty' pparams in
let fixed =
- C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
+ C.ADefinition (xid,id,te,ty,C.Actual real_params)
in
Xml.pp (Cic2Xml.pp fixed uri) filename ;
| _ -> ()