X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=af3999a3963df8fd1aa714dce8ab6f86c2f394bc;hb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;hp=0fbd5e458e777b25270c849f9dad6edc5365067b;hpb=399f84005987d007bd24f8a0dea3bb2211070a18;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 0fbd5e458..af3999a39 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -32,6 +32,16 @@
 (*                                                                         *)
 (***************************************************************************)
 
+let p_mtr a b = Mpresentation.Mtr(a,b)
+let p_mtd a b = Mpresentation.Mtd(a,b)
+let p_mtable a b = Mpresentation.Mtable(a,b)
+let p_mtext a b = Mpresentation.Mtext(a,b)
+let p_mi a b = Mpresentation.Mi(a,b)
+let p_mo a b = Mpresentation.Mo(a,b)
+let p_mrow a b = Mpresentation.Mrow(a,b)
+let p_mphantom a b = Mpresentation.Mphantom(a,b)
+
+
 let rec split n l =
   if n = 0 then [],l
   else let l1,l2 = 
@@ -400,8 +410,8 @@ and proof2pres term2pres p =
          | _ -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
-          P.Mrow []
-           [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+          p_mrow []
+           [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
        | Some c -> let conclusion = term2pres c in
           make_row 
             [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
@@ -777,103 +787,103 @@ let content2pres term2pres (id,params,metasenv,obj) =
  let module P = Mpresentation in
   match obj with
      `Def (K.Const,thesis,`Proof p) ->
-       P.Mtable
+       p_mtable
         [None,"align","baseline 1";
          None,"equalrows","false";
          None,"columnalign","left";
          None,"helm:xref","id"]
-        ([P.Mtr []
-           [P.Mtd []
-            (P.Mrow []
-             [P.Mtext []
+        ([p_mtr []
+           [p_mtd []
+            (p_mrow []
+             [p_mtext []
                ("UNFINISHED PROOF" ^ id ^"(" ^
                  String.concat " ; " (List.map UriManager.string_of_uri params)^
                 ")")])] ;
-         P.Mtr []
-          [P.Mtd []
-            (P.Mrow []
-              [P.Mtext [] "THESIS:"])] ;
-         P.Mtr []
-          [P.Mtd []
-            (P.Mrow []
-              [P.Mphantom []
-                (P.Mtext [] "__") ;
+         p_mtr []
+          [p_mtd []
+            (p_mrow []
+              [p_mtext [] "THESIS:"])] ;
+         p_mtr []
+          [p_mtd []
+            (p_mrow []
+              [p_mphantom []
+                (p_mtext [] "__") ;
               term2pres thesis])]] @
          (match metasenv with
              None -> []
            | Some metasenv' ->
-              [P.Mtr []
-                [P.Mtd []
+              [p_mtr []
+                [p_mtd []
                   (* Conjectures are in their own table to make *)
                   (* diffing the DOM trees easier.              *)
-                  (P.Mtable
+                  (p_mtable
                     [None,"align","baseline 1";
                      None,"equalrows","false";
                      None,"columnalign","left"]
-                   ((P.Mtr []
-                      [P.Mtd []
-                       (P.Mrow []
-                         [P.Mtext [] "CONJECTURES:"])])::
+                   ((p_mtr []
+                      [p_mtd []
+                       (p_mrow []
+                         [p_mtext [] "CONJECTURES:"])])::
                     List.map
                      (function
                        (id,n,context,ty) ->
-                         P.Mtr []
-                          [P.Mtd []
-                           (P.Mrow [Some "helm", "xref", id]
+                         p_mtr []
+                          [p_mtd []
+                           (p_mrow [Some "helm", "xref", id]
                              (List.map
                                (function
                                    None ->
-                                     P.Mrow []
-                                      [ P.Mi [] "_" ;
-                                        P.Mo [] ":?" ;
-                                        P.Mi [] "_"]
+                                     p_mrow []
+                                      [ p_mi [] "_" ;
+                                        p_mo [] ":?" ;
+                                        p_mi [] "_"]
                                  | Some (`Declaration d)
                                  | Some (`Hypothesis d) ->
                                     let
                                      { K.dec_name = dec_name ;
                                        K.dec_type = ty } = d
                                      in
-                                      P.Mrow []
-                                       [ P.Mi []
+                                      p_mrow []
+                                       [ p_mi []
                                           (match dec_name with
                                               None -> "_"
                                             | Some n -> n) ;
-                                         P.Mo [] ":" ;
+                                         p_mo [] ":" ;
                                          term2pres ty]
                                  | Some (`Definition d) ->
                                     let
                                      { K.def_name = def_name ;
                                        K.def_term = bo } = d
                                      in
-                                      P.Mrow []
-                                       [ P.Mi []
+                                      p_mrow []
+                                       [ p_mi []
                                           (match def_name with
                                               None -> "_"
                                             | Some n -> n) ;
-                                         P.Mo [] ":=" ;
+                                         p_mo [] ":=" ;
                                          term2pres bo]
                                  | Some (`Proof p) ->
                                     let proof_name = p.K.proof_name in
-                                     P.Mrow []
-                                      [ P.Mi []
+                                     p_mrow []
+                                      [ p_mi []
                                          (match proof_name with
                                              None -> "_"
                                            | Some n -> n) ;
-                                        P.Mo [] ":=" ;
+                                        p_mo [] ":=" ;
                                         proof2pres term2pres p]
                                ) (List.rev context) @
-                             [ P.Mo [] "|-" ] @
-                             [ P.Mi [] (string_of_int n) ;
-                               P.Mo [] ":" ;
+                             [ p_mo [] "|-" ] @
+                             [ p_mi [] (string_of_int n) ;
+                               p_mo [] ":" ;
                                term2pres ty ]
                            ))
                           ]
                      ) metasenv'
                   ))]]
          )  @
-        [P.Mtr []
-          [P.Mtd []
-            (P.Mrow []
+        [p_mtr []
+          [p_mtd []
+            (p_mrow []
               [proof2pres term2pres p])]])
    | _ -> raise ToDo
 ;;