X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=b1b38a9492e76cb5526c24c870382696a5f50314;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=94ef66c952509257b70371333a5f9d3c6c990bbb;hpb=3a841c391df854fa4397521d9bcd775a7804d84e;p=helm.git

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