C.Prod (name, deannotate_term so, deannotate_term ta)
| C.ALambda (_,name,so,ta) ->
C.Lambda (name, deannotate_term so, deannotate_term ta)
- | C.ALetIn (_,name,so,ta) ->
- C.LetIn (name, deannotate_term so, deannotate_term ta)
+ | C.ALetIn (_,name,so,ty,ta) ->
+ C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta)
| C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
| C.AConst (_,uri,exp_named_subst) ->
let deann_exp_named_subst =
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 (ate,aty))) ->
+ Some(n,(C.Def(deannotate_term ate,deannotate_term aty)))
+ | _,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) ->