List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
;;
+let deannotate_conjectures =
+ let module C = Cic in
+ List.map
+ (function
+ (_,id,acontext,con) ->
+ let context =
+ List.map
+ (function
+ | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None)))
+ | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
+ | _,None -> None)
+ acontext
+ in
+ (id,context,deannotate_term con))
+;;
+
let deannotate_obj =
let module C = Cic in
function
| C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
C.CurrentProof (
name,
- List.map
- (function
- (_,id,acontext,con) ->
- let context =
- List.map
- (function
- _,Some (n,(C.ADef at)) ->
- Some (n,(C.Def ((deannotate_term at),None)))
- | _,Some (n,(C.ADecl at)) ->
- Some (n,(C.Decl (deannotate_term at)))
- | _,None -> None
- ) acontext
- in
- (id,context,deannotate_term con)
- ) conjs,
+ deannotate_conjectures conjs,
deannotate_term bo,deannotate_term ty, params, attrs
)
| C.AInductiveDefinition (_, tys, params, parno, attrs) ->