From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Nov 2006 18:57:26 +0000 (+0000)
Subject: Added a clear to rewritestep to speed up auto (by removing an hypothesis
X-Git-Tag: 0.4.95@7852~767
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18c16056c2858405c899ab027ec7e7ba2cc967b4;hp=218a5af368cb7ea58c59cad2e7c8ef1f733792c2;p=helm.git

Added a clear to rewritestep to speed up auto (by removing an hypothesis
that must NOT be used again).
---

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 94ef66c95..b1b38a949 100644
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -175,7 +175,9 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude =
                 ~continuations:
                   [ Tactics.apply prhs ;
                     Tactics.apply (Cic.Rel 1) ;
-                    just]) status
+                    Tacticals.then_
+                     ~start:(Tactics.clear ~hyps:[last_hyp_name])
+                     ~continuation:just]) status
           | Some name ->
              let mk_fresh_name_callback =
 	      fun metasenv context _ ~typ ->
@@ -193,7 +195,9 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude =
                       ~continuations:
                         [ Tactics.apply prhs ;
                           Tactics.apply (Cic.Rel 1) ;
-                          just]
+                          Tacticals.then_
+                           ~start:(Tactics.clear ~hyps:[last_hyp_name])
+                           ~continuation:just]
                    ]) status)
     | Some lhs ->
        match conclude with