C.LetIn (name, deannotate_term so, deannotate_term ta)
| C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
| C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno)
C.LetIn (name, deannotate_term so, deannotate_term ta)
| C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
| C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno)
| C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
| C.AMutConstruct (_,uri,cookingsno,i,j) ->
C.MutConstruct (uri,cookingsno,i,j)
| C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
| C.AMutConstruct (_,uri,cookingsno,i,j) ->
C.MutConstruct (uri,cookingsno,i,j)
- 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
)
| C.AInductiveDefinition (_, tys, params, parno) ->
C.InductiveDefinition ( List.map deannotate_inductiveType tys,
)
| C.AInductiveDefinition (_, tys, params, parno) ->
C.InductiveDefinition ( List.map deannotate_inductiveType tys,