From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 24 Jul 2003 13:19:20 +0000 (+0000)
Subject: The name of TD proofs was erroneously always set to previous.
X-Git-Tag: LucaOK~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=135dd1812b3c512cb2d82ba9781e1b4489cdbc04

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