name,
List.map
(function
- (id,acontext,con) ->
+ (_,id,acontext,con) ->
let context =
List.map
(function
- Some (n,(C.ADef at)) -> Some (n,(C.Def (deannotate_term at)))
- | Some (n,(C.ADecl at)) ->Some (n,(C.Decl (deannotate_term at)))
- | None -> None) acontext
+ _,Some (n,(C.ADef at)) ->
+ Some (n,(C.Def (deannotate_term at)))
+ | _,Some (n,(C.ADecl at)) ->
+ Some (n,(C.Decl (deannotate_term at)))
+ | _,None -> None
+ ) acontext
in
- (id,context, deannotate_term con)
+ (id,context,deannotate_term con)
) conjs,
- deannotate_term bo, deannotate_term ty
+ deannotate_term bo,deannotate_term ty
)
| C.AInductiveDefinition (_, tys, params, parno) ->
C.InductiveDefinition ( List.map deannotate_inductiveType tys,