X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=bd846248b848f0d2162038de0c5b627fa010bead;hb=70aa6dc959dc1d49f751c183367c3b73393c938b;hp=4ea07a54f0dc278ac2a6f20f2619e1cfb8f24ea6;hpb=cee0c3ca597ebbff2250674c255ed1bc909521fb;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 4ea07a54f..bd846248b 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -187,16 +187,11 @@ let pp_ncommand = function
       pp_notation dir_opt l1_pattern assoc prec l2_pattern
 ;;
     
-let pp_command = function
-  | Print (_,s) -> "print " ^ s
-  | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
-
 let pp_executable ~map_unicode_to_tex =
   function
   | NMacro (_, macro) -> pp_nmacro macro ^ "."
   | NTactic (_,tacl) ->
       String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl)
-  | Command (_, cmd) -> pp_command cmd ^ "."
   | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
                       
 let pp_comment ~map_unicode_to_tex =