Use of standard OCaml syntax

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

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 42d7df86492625b3b8c00340affcce2f5ad995e2..aade1a07970d95f8b74d0b6f98dd46cd9f9278c8 100644 (file)
--- 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) -> "@ " ^
@@ -86,13 +86,13 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
       String.concat " " (List.map (NotationPp.pp_term status) l)
   | NCase1 (_,n) -> "*" ^ n ^ ":"
-  | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
+  | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ 
       " with " ^ NotationPp.pp_term status wwhat
   | NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
   | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
   | NClear (_,l) -> "nclear " ^ String.concat " " l
-  | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+  | NDestruct (_,_dom,_skip) -> "ndestruct ..." 
   | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
       "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NId _ -> "nid"