- | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
- let proof = (aux bo) in (* must be recursive !! *)
- { K.proof_name = name;
- K.proof_id = gen_id seed;
- K.proof_context = [`Proof proof];
- K.proof_apply_context = [];
- K.proof_conclude =
- { K.conclude_id = gen_id seed;
- K.conclude_aref = id;
- K.conclude_method = "Exact";
- K.conclude_args =
- [ K.Premise
- { K.premise_id = gen_id seed;
- K.premise_xref = proof.K.proof_id;
- K.premise_binder = proof.K.proof_name;
- K.premise_n = Some 1;
- }
- ];
- K.conclude_conclusion =
- try Some
- (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
- with Not_found -> None
- }
- }