]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/ast2pres.ml
debian version 0.0.6-6
[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml
index 9fc2533aefecf84b405d2c99d76c820e7865ad14..470019835472be0a7880294d36f4c4a0e5163b59 100644 (file)
@@ -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)]