X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=c88f87535f71fe71aa6aac2e539060ad8cea7ae6;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=9c389467c1f6cef38b4bd03536040ed599024033;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 9c389467c..c88f87535 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in [B.H([], - (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by")):: + (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*) + (B.b_kw "by"):: B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")])], None else