The name of TD proofs was erroneously always set to previous.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0e0edf100066ec9ceaa616f001092972ca392ae7..21b39fe65209372c21cd6078fe205ce33084d18b 100644 (file)
--- 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
               };
           }