X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=0cc52ac1ab523a8cd7464619dde45d143709a8a4;hb=5c10d402b5de7233bc83d7f685b274832e383212;hp=79e627409ed5794f451f23b40c13316bde7e3379;hpb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 79e627409..0cc52ac1a 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -196,7 +196,8 @@ let rewritingstep ~dbd ~automation_cache lhs rhs just last_step =
             Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
     | `Term just -> Tactics.apply just
     | `SolveWith term -> 
-         Tactics.solve_rewrite ~automation_cache ~params:([term],["steps","1"]) ()
+                    Tactics.solve_rewrite ~automation_cache
+                    ~params:([term],["steps","1"; "use_context","false"]) ()
     | `Proof ->
         Tacticals.id_tac
   in