Matitaweb: fixes compilation errors and minor graphical problems.

[helm.git] / matitaB / components / grafite / grafiteAstPp.ml

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index 78bb51971e1ab5ec595f370be2b519d831d6bf95..d4d312bd2b455c38489f81c50ee53e046f1cfd0f 100644 (file)
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -59,7 +59,7 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
-  | NAuto (_,(Some l,flgs)) ->
+  | NAuto (_,(Some (_,l),flgs)) ->
       "nautobatch" ^ " by " ^
          (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)