X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=21b39fe65209372c21cd6078fe205ce33084d18b;hb=135dd1812b3c512cb2d82ba9781e1b4489cdbc04;hp=0e0edf100066ec9ceaa616f001092972ca392ae7;hpb=6baf07f7ebd9b40e642467f01a66920d9fb1448a;p=helm.git

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
               };
           }