| None ->
C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
| `Proof p ->
+ let ty =
+ match p.Con.proof_conclude.Con.conclude_conclusion with
+ None -> (*Cic.Implicit None*) assert false
+ | Some ty -> deannotate ty
+ in
(match p.Con.proof_name with
Some s ->
- C.LetIn (C.Name s, proof2cic premise_env p, target)
+ C.LetIn (C.Name s, proof2cic premise_env p, ty , target)
| None ->
- C.LetIn (C.Anonymous, proof2cic premise_env p, target))
+ C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target))
| `Definition d ->
(match d.Con.def_name with
Some s ->
- C.LetIn (C.Name s, proof2cic premise_env p, target)
+ C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target)
| None ->
- C.LetIn (C.Anonymous, proof2cic premise_env p, target))
+ C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target))
| `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
(match target with
C.Rel n ->
| _ -> 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))
+ {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} ->
+ Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty))
| _ -> assert false)
| Some (`Proof d) ->
(match d with
{K.proof_name = Some n } ->
Some (Cic.Name n,
- Cic.Def ((proof2cic deannotate d),None))
+ Cic.Def ((proof2cic deannotate d),assert false))
| _ -> assert false)
) canonical_context
in