From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:05:55 +0000 (+0000) Subject: Bug fixed: name in letin was printed as "previous" even if given. X-Git-Tag: make_still_working~6224 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ca5e357b247833e561be0f0760d18d705d4f1d6;p=helm.git Bug fixed: name in letin was printed as "previous" even if given. --- 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) ->