None -> inner_proof
| Some expty ->
if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
- { K.proof_name = None ;
+ { K.proof_name = inner_proof.K.proof_name;
K.proof_id = gen_id seed;
K.proof_context = [] ;
K.proof_apply_context = [];
{ K.conclude_id = gen_id seed;
K.conclude_aref = id;
K.conclude_method = "TD_Conversion";
- K.conclude_args = [K.ArgProof inner_proof];
+ K.conclude_args =
+ [K.ArgProof {inner_proof with K.proof_name = None}];
K.conclude_conclusion = Some expty
};
}