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: make_still_working~6626
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=12404305178bb29f7428ba912fce30c524076705;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/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 94ef66c95..b1b38a949 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/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