X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=f489b15b5e399667c655ea336a39fba0d5a9b7b0;hb=d0c7735ccdde99179105d56a8fafa22060aa6184;hp=e022c6f33114c122bac42f2e1ba6e6a99918b3d7;hpb=d272210a331d720b08d50b845fa21fa7ec0d4252;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index e022c6f33..f489b15b5 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -77,10 +77,10 @@ let opt_string_pp = function
 let pp_auto_params ~term_pp (univ, params) = 
    String.concat " " 
      (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
-   if univ <> [] then 
-     (if params <> [] then " " else "") ^ "by " ^ 
-     String.concat " " (List.map term_pp univ)
-   else ""
+     match univ with
+       | None -> ""
+       | Some l -> (if params <> [] then " " else "") ^ "by " ^ 
+	   String.concat " " (List.map term_pp l)
 ;;
 
 let pp_just ~term_pp =
@@ -96,10 +96,12 @@ let rec pp_ntactic ~map_unicode_to_tex =
   pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
  function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
-  | NAuto (_,(l,flgs)) ->
-      "nauto" ^ 
-        (if l <> [] then (" by " ^
-         (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
+  | NAuto (_,(None,flgs)) ->
+      "nauto" ^
+        String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+  | NAuto (_,(Some l,flgs)) ->
+      "nauto" ^ " by " ^
+         (String.concat "," (List.map CicNotationPp.pp_term l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false