From 135dd1812b3c512cb2d82ba9781e1b4489cdbc04 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 24 Jul 2003 13:19:20 +0000 Subject: [PATCH] The name of TD proofs was erroneously always set to previous. --- helm/ocaml/cic_omdoc/cic2content.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 0e0edf100..21b39fe65 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -243,7 +243,7 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = 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 = []; @@ -251,7 +251,8 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = { 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 }; } -- 2.39.2