X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=f869801f97296b4d7ebad0d7f15bf3c0922f6d1e;hb=53a5acbe28212706be9c684d612aee1ccb165587;hp=05e4ae3cbd8d55532a9cb51ba41b3324989f8389;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index 05e4ae3cb..f869801f9 100644
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -881,36 +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 recursion_kind2pres params kind =
-  let kind =
-    match kind with
-    | `Recursive _ -> "Recursive definition"
-    | `CoRecursive -> "CoRecursive definition"
-    | `Inductive i -> 
-        "Inductive definition with "^string_of_int i^" fixed parameter(s)"
-    | `CoInductive i -> 
-        "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)"
-  in
-  B.b_h [] (B.b_kw kind :: params2pres params)
-;;
-
 let inductive2pres term2pres ind =
   let constructor2pres decl =
     B.b_h [] [
@@ -930,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 
@@ -970,12 +940,6 @@ let definition2pres ?recno term2pres d =
    B.b_h [] [B.b_space;term2pres body] ]
 ;;
 
-let joint_def2pres ?recno term2pres def =
-  match def with
-  | `Inductive ind -> inductive2pres term2pres ind
-  | _ -> assert false
-;;
-
 let njoint_def2pres ?recno term2pres def =
   match def with
   | `Inductive ind -> inductive2pres term2pres ind
@@ -1012,66 +976,9 @@ let njoint_def2pres term2pres joint_kind defs =
           (List.map (njoint_def2pres term2pres) defs)))
 ;;
 
-let content2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
-  (id,params,metasenv,obj) 
-=
-  match obj with
-  | `Def (Content.Const, thesis, `Proof p) ->
-      let name = get_name p.Content.proof_name in
-      let proof = proof2pres true term2pres ?skip_initial_lambdas p in
-      if skip_thm_and_qed then
-        proof
-      else
-      B.b_v
-        [Some "helm","xref","id"]
-        ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: 
-          params2pres params @ [B.b_kw ":"]);
-           B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @
-         metasenv2pres term2pres metasenv @
-         [proof ; B.b_kw "qed."])
-  | `Def (_, ty, `Definition body) ->
-      let name = get_name body.Content.def_name in
-      B.b_v
-        [Some "helm","xref","id"]
-        ([B.b_h []
-           (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]);
-          B.indent (term2pres ty)] @
-          metasenv2pres term2pres metasenv @
-          [B.b_kw ":=";
-           B.indent (term2pres body.Content.def_term);
-           B.b_kw "."])
-  | `Decl (_, `Declaration decl)
-  | `Decl (_, `Hypothesis decl) ->
-      let name = get_name decl.Content.dec_name in
-      B.b_v
-        [Some "helm","xref","id"]
-        ([B.b_h [] (B.b_kw ("axiom " ^ name) :: params2pres params);
-          B.b_kw "Type:";
-          B.indent (term2pres decl.Content.dec_type)] @
-          metasenv2pres term2pres metasenv)
-  | `Joint joint ->
-      B.b_v []
-        (recursion_kind2pres params joint.Content.joint_kind
-        :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
-  | _ -> raise ToDo
-
-let content2pres 
-  ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
-=
-  content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
-    (fun ?(prec=90) annterm ->
-      let ast, ids_to_uris =
-       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
-      in
-       CicNotationPres.box_of_mpres
-        (CicNotationPres.render
-          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
-          (TermContentPres.pp_ast ast)))
-
 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) ->
@@ -1083,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."])
@@ -1092,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 ":=";
@@ -1103,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)