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 94ef66c952509257b70371333a5f9d3c6c990bbb..b1b38a9492e76cb5526c24c870382696a5f50314 100644 (file)
--- 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