X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=aade1a07970d95f8b74d0b6f98dd46cd9f9278c8;hb=926bd86002f91d2bf2a3ce7376309f5106268959;hp=e16ce39bd5e5b11ad3901c99455991b48709d762;hpb=66be8fbe19e2ccfa0e6a7abeba605152d1322595;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index e16ce39bd..aade1a079 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -53,9 +53,9 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) =
 
 let pp_auto_params params status =
     match params with
-    | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+    | (None,flags) -> String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flags)
     | (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
-    String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+    String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flags)
 ;;
 
 let pp_just status just =
@@ -74,11 +74,11 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NSmartApply (_,_t) -> "fixme"
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
-        String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+        String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) 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)
+        String.concat " " (List.map (fun (a,b) -> a ^ "=" ^ b) flgs)
   | NCases (_,what,_where) -> "ncases " ^ NotationPp.pp_term status what ^
       "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NConstructor (_,None,l) -> "@ " ^