X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=6d8031d85b4e67d3f71b1001d224f02db92ede61;hb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;hp=617c9ddcacbb6fa0aed9dfd47e5f3b68d0db740b;hpb=bfcde2b08d72f1392ed61164c67d199360f0397f;p=helm.git

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index 617c9ddca..6d8031d85 100644
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -881,22 +881,6 @@ let metasenv2pres term2pres = function
             (let _ = incr counter; in (string_of_int !counter)))) ::
          (List.map (conjecture2pres term2pres) metasenv'))]
 
-let params2pres params =
-  let param2pres uri =
-    B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
-      (UriManager.name_of_uri uri)
-  in
-  let rec spatiate = function
-    | [] -> []
-    | hd :: [] -> [hd]
-    | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
-  in
-  match params with
-  | [] -> []
-  | p ->
-      let params = spatiate (List.map param2pres p) in
-      [B.b_space;
-       B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
 let inductive2pres term2pres ind =
   let constructor2pres decl =
     B.b_h [] [
@@ -916,7 +900,7 @@ let definition2pres ?recno term2pres d =
   let name = match d.Content.def_name with Some x -> x|_->assert false in
   let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
-  let module P = CicNotationPt in
+  let module P = NotationPt in
   let rec split_pi i t = 
     if i <= 1 then 
       match t with 
@@ -994,7 +978,7 @@ let njoint_def2pres term2pres joint_kind defs =
 
 let ncontent2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
-  (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
+  (id,metasenv,obj : NotationPt.term Content.cobj) 
 =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
@@ -1006,7 +990,7 @@ let ncontent2pres0
       B.b_v
         [Some "helm","xref","id"]
         ([ B.b_h [] (B.b_kw ("ntheorem " ^ name) :: 
-          params2pres params @ [B.b_kw ":"]);
+          [B.b_kw ":"]);
            B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @
          metasenv2pres term2pres metasenv @
          [proof ; B.b_kw "qed."])
@@ -1015,7 +999,7 @@ let ncontent2pres0
       B.b_v
         [Some "helm","xref","id"]
         ([B.b_h []
-           (B.b_kw ("ndefinition " ^ name) :: params2pres params @ [B.b_kw ":"]);
+           (B.b_kw ("ndefinition " ^ name) :: [B.b_kw ":"]);
           B.indent (term2pres ty)] @
           metasenv2pres term2pres metasenv @
           [B.b_kw ":=";
@@ -1026,7 +1010,7 @@ let ncontent2pres0
       let name = get_name decl.Content.dec_name in
       B.b_v
         [Some "helm","xref","id"]
-        ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: params2pres params);
+        ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: []);
           B.b_kw "Type:";
           B.indent (term2pres decl.Content.dec_type)] @
           metasenv2pres term2pres metasenv)
@@ -1036,7 +1020,7 @@ let ncontent2pres0
           joint.Content.joint_kind joint.Content.joint_defs]
   | _ -> raise ToDo
 
-let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
+let ncontent2pres status ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
  let lookup_uri id =
   try
    let nref = Hashtbl.find ids_to_nrefs id in
@@ -1046,4 +1030,5 @@ let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
   ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) ast ->
       CicNotationPres.box_of_mpres
-       (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))
+       (CicNotationPres.render ~lookup_uri ~prec
+         (TermContentPres.pp_ast status ast)))