]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPres.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationPres.ml
index 790bb3785088a8b67c7dc905fcefa66919d8b4bd..83bb10878518d0e0eb7eeda8fb1e410e5516e722 100644 (file)
@@ -142,8 +142,8 @@ let is_atomic t =
   aux_mpres t
 
 let add_parens child_prec child_assoc child_pos curr_prec t =
-  prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec
-    (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec));
+(*  prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec
+    (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); *)
   if is_atomic t then t
   else if child_prec < curr_prec
     || (child_prec = curr_prec &&
@@ -211,7 +211,6 @@ let render ids_to_uris =
         add_parens child_prec child_assoc pos prec t'
     | `IdRef xref -> aux mathonly (Some xref) pos prec uris t
     | `Href uris' -> aux mathonly xref pos prec uris' t
-    | _ -> assert false
   and aux_literal xref prec uris l =
     let attrs = make_href xref uris in
       match l with