exception NotExpectingPossibleParameters;;
+(* converts annotated terms into cic terms (forgetting ids and names) *)
let rec deannotate_term =
let module C = Cic in
function
C.ARel (_,n,_) -> C.Rel n
| C.AVar (_,uri) -> C.Var uri
- | C.AMeta (_,n) -> C.Meta n
+ | C.AMeta (_,n, l) ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some at -> Some (deannotate_term at)
+ ) l
+ in
+ C.Meta (n, l')
| C.ASort (_,s) -> C.Sort s
| C.AImplicit _ -> C.Implicit
| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
deannotate_term ty)
| C.ACurrentProof (_, name, conjs, bo, ty) ->
C.CurrentProof (
- name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
+ name,
+ List.map
+ (function
+ (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
+ in
+ (id,context, deannotate_term con)
+ ) conjs,
deannotate_term bo, deannotate_term ty
)
| C.AInductiveDefinition (_, tys, params, parno) ->