arithmetics for λδ

[helm.git] / matitaB / components / content_pres / cicNotationPres.ml

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index e0ca07b563ab6c64c651e139cf4a8b5e10dd0e8a..553ab1ae1ba2aa352439e0935255e8318eff52d5 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -130,9 +130,9 @@ let render status ?(prec=(-1)) =
         Box.H ([],
           (Box.Text ([], "?"^string_of_int n)::
             (if (l <> []) then [Box.H ([],local_context)] else [])))
-    | A.Literal (`Symbol (s,x))
-    | A.Literal (`Keyword (s,x))
-    | A.Literal (`Number (s,x)) ->
+    | A.Literal (_,`Symbol (s,x))
+    | A.Literal (_,`Keyword (s,x))
+    | A.Literal (_,`Number (s,x)) ->
        let attr = 
          match x with
          | None, None -> []
@@ -249,7 +249,7 @@ let render status ?(prec=(-1)) =
       List.map boxify_pres (find_clusters terms) 
   in
   (fun t ->
-          prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));
+   (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
   aux prec t)
 
 (* let render_to_boxml id_to_uri t =