X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=45e88ab0a26a9fc5626fc1a86bf6565d2477a9df;hb=1ca5e357b247833e561be0f0760d18d705d4f1d6;hp=ee11e9b6d76c36690c31a20474620bce5a842208;hpb=82d0bc4291648c88e9f248fc5a67518e938eacdf;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index ee11e9b6d..45e88ab0a 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -113,9 +113,9 @@ let make_args_for_apply term2pres args =
         (List.fold_right (make_arg_for_apply false) tl [])
   | _ -> assert false
 
-let get_name = function
+let get_name ?(default="_") = function
   | Some s -> s
-  | None -> "_"
+  | None -> default
 
 let add_xref id = function
   | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t)
@@ -345,7 +345,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                  ((if not is_top_down || omit_dot then
                     (make_concl "we proved" concl) ::
                       if not is_top_down then
-                       [B.b_space; B.Text([],"(previous)")]
+                       let name = get_name ~default:"previous" name in
+                        [B.b_space; B.Text([],"(" ^ name ^ ")")]
                       else []
                    else [B.b_kw "done"]
                   ) @ if not omit_dot then [B.Text([],".")] else [])
@@ -524,7 +525,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
             Con.Aux n -> B.b_kw "an aux???"
            | Con.Premise prem ->
               (match prem.Con.premise_binder with
-                 None -> B.b_kw "the previous result"
+                 None -> B.b_kw "previous"
                | Some n -> B.Object ([], P.Mi([],n)))
            | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
            | Con.Term (_,t) -> 
@@ -555,7 +556,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
             Con.Aux n -> B.b_kw "an aux???"
            | Con.Premise prem ->
               (match prem.Con.premise_binder with
-                 None -> B.b_kw "the previous result"
+                 None -> B.b_kw "previous"
                | Some n -> B.Object ([], P.Mi([],n)))
            | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
            | Con.Term (_,t) ->