From 18c16056c2858405c899ab027ec7e7ba2cc967b4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Nov 2006 18:57:26 +0000 Subject: [PATCH] Added a clear to rewritestep to speed up auto (by removing an hypothesis that must NOT be used again). --- components/tactics/declarative.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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 -- 2.39.2