| 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 ->
| _ -> prerr_endline "2"; assert false)
else if conclude.Con.conclude_method = "Exact" then
(match conclude.Con.conclude_args with
- [Con.Term t] -> deannotate t
+ [Con.Term (_,t)] -> deannotate t
| [Con.Premise prem] ->
(match prem.Con.premise_n with
None -> assert false
conclude.Con.conclude_method = "Exists" ||
conclude.Con.conclude_method = "FalseInd") then
(match (List.tl conclude.Con.conclude_args) with
- Con.Term (C.AAppl (
+ Con.Term (_,C.AAppl (
id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
| _ -> prerr_endline "5"; assert false)
else if (conclude.Con.conclude_method = "Rewrite") then
(match conclude.Con.conclude_args with
- Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
+ Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in
| _ -> prerr_endline "6"; assert false)
else if (conclude.Con.conclude_method = "Case") then
(match conclude.Con.conclude_args with
- Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+ Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Premise(prem)::patterns ->
C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty,
(function
Con.ArgProof p -> proof2cic [] p
| _ -> prerr_endline "7a"; assert false) patterns)
- | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
+ | Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Term(_,te)::patterns -> C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty, deannotate te,
List.map
raise Not_found))
| Con.Lemma lemma ->
CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
- | Con.Term t -> deannotate t
+ | Con.Term (_,t) -> deannotate t
| Con.ArgProof p -> proof2cic [] p (* empty! *)
| Con.ArgMethod s -> raise TO_DO
| _ -> 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