X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=d9255f220d02247026943886f1515e96d1194a27;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=9c389467c1f6cef38b4bd03536040ed599024033;hpb=07713b63c109a99c2b9dc7265571bcdd3dd6ed0d;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 9c389467c..d9255f220 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
@@ -957,11 +958,14 @@ let definition2pres ?recno term2pres d =
       params
   in
   B.b_hv [] 
-   [B.b_hv [] 
-    ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
-    (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
-    @[ B.b_space;
-       B.b_text [] ":"; B.b_space; term2pres ty]); 
+   [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
+    ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ 
+        [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] 
+      @ [B.b_h [] 
+         ((if rno <> -1 then 
+           [B.b_kw "on";B.b_space;term2pres rec_param] else [])
+         @ [ B.b_space; B.b_text [] ":";]) ]
+      @[ B.indent(term2pres ty)]); 
    B.b_text [] ":=";
    B.b_h [] [B.b_space;term2pres body] ]
 ;;
@@ -1009,7 +1013,8 @@ let njoint_def2pres term2pres joint_kind defs =
 ;;
 
 let content2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj) 
 =
   match obj with
@@ -1066,7 +1071,8 @@ let content2pres
           (TermContentPres.pp_ast ast)))
 
 let ncontent2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with