| Some (`Definition d) ->
(match d with
{K.def_name = Some n ; K.def_term = t} ->
- Some (Cic.Name n, Cic.Def (deannotate 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))
+ Some (Cic.Name n,
+ Cic.Def ((proof2cic deannotate d),None))
| _ -> assert false)
) canonical_context
in