demodulate takes an extra argument 'all', if present it attempts to solve

[helm.git] / helm / software / components / tactics / declarative.ml

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 79e627409ed5794f451f23b40c13316bde7e3379..0cc52ac1ab523a8cd7464619dde45d143709a8a4 100644 (file)
--- 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