X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=a333dccfcecd8af573db0036858b0347e492ddd5;hb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;hp=9e08fb3b5f78377e1dea320faa080c9c8011d5a1;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 9e08fb3b5..a333dccfc 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -147,7 +147,7 @@ let rec pp_ntactic status ~map_unicode_to_tex =
       ^ "=" ^
       NotationPp.pp_term status term1 ^ 
       (match term2 with 
-      | `Auto params -> pp_auto_params (None,params) status
+      | `Auto params -> pp_auto_params params status
       | `Term term2 -> " exact " ^ NotationPp.pp_term status term2 
       | `Proof -> " proof"
       | `SolveWith term -> " using " ^ NotationPp.pp_term status term)