X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=470019835472be0a7880294d36f4c4a0e5163b59;hb=a864255e782859e2b3b7da08297f5d3fe2ee710d;hp=9fc2533aefecf84b405d2c99d76c820e7865ad14;hpb=3b22e6ed78aa7d1d076734a7e91ef6f2066a4aa9;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 9fc2533ae..470019835 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -100,7 +100,8 @@ let is_big t =
 
 let map_attribute =
   function
-      `Loc (n,m) -> 
+      `Loc floc -> 
+        let (n, m) = CicAst.loc_of_floc floc in
         (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
     | `IdRef s -> 
         (Some "helm","xref",s)
@@ -153,14 +154,14 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                                 Box.smallskip; 
                                  make_pattern constr vars;
                                 Box.smallskip; 
-                                Box.Text([],"\Rightarrow")]);
+                                Box.Text([],"\\Rightarrow")]);
                       Box.indent (bigast2box rhs)])
           else
             Box.H([],[Box.Text([],sep);
                       Box.smallskip; 
                       make_pattern constr vars;
                       Box.smallskip; 
-                      Box.Text([],"\Rightarrow");
+                      Box.Text([],"\\Rightarrow");
                       Box.smallskip; 
                       Box.Object([],rhs)]) in
         let plbox = match pl with
@@ -305,7 +306,7 @@ and make_subst start_txt varname body end_txt =
     [Box.Text([],start_txt);
      Box.Text([],varname);
      Box.smallskip;
-     Box.Text([],"\Assign")
+     Box.Text([],"\\Assign")
     ]
     body
     [Box.Text([],end_txt)]