+let cobj2obj deannotate (id,params,metasenv,obj) =
+ let module K = Content in
+ match obj with
+ `Def (Content.Const,ty,`Proof bo) ->
+ (match metasenv with
+ None ->
+ Cic.Constant
+ (id, Some (proof2cic deannotate bo), deannotate ty, params)
+ | Some metasenv' ->
+ let metasenv'' =
+ List.map
+ (function (_,i,canonical_context,term) ->
+ let canonical_context' =
+ List.map
+ (function
+ None -> None
+ | Some (`Declaration d)
+ | Some (`Hypothesis d) ->
+ (match d with
+ {K.dec_name = Some n ; K.dec_type = t} ->
+ Some (Cic.Name n, Cic.Decl (deannotate t))
+ | _ -> assert false)
+ | Some (`Definition d) ->
+ (match d with
+ {K.def_name = Some n ; K.def_term = t} ->
+ Some (Cic.Name n, Cic.Def ((deannotate t),None))
+ | _ -> assert false)
+ | Some (`Proof d) ->
+ (match d with
+ {K.proof_name = Some n } ->
+ Some (Cic.Name n,
+ Cic.Def ((proof2cic deannotate d),None))
+ | _ -> assert false)
+ ) canonical_context
+ in
+ (i,canonical_context',deannotate term)
+ ) metasenv'
+ in
+ Cic.CurrentProof
+ (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+ | _ -> raise ToDo
+;;