Changes to declarative tactics, implementation of equality chain

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

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 9e08fb3b5f78377e1dea320faa080c9c8011d5a1..a333dccfcecd8af573db0036858b0347e492ddd5 100644 (file)
--- 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)