This is a reworking of the previous rewrite equiv tactic, hopefully addressing the points made in #362. Its task has been simplified and now simply focusses on a particular call statement rather than attempting to match program slices with function bodies. This latter task has been offloaded to the new outline tactic.
The other main change to the tactic is that only one memory is used at a time. I found this increases flexibility of the tactic (see the various changes in stdlib/examples) and, for me, was more intuitive to use.
This is a reworking of the previous
rewrite equivtactic, hopefully addressing the points made in #362. Its task has been simplified and now simply focusses on a particular call statement rather than attempting to match program slices with function bodies. This latter task has been offloaded to the newoutlinetactic. The other main change to the tactic is that only one memory is used at a time. I found this increases flexibility of the tactic (see the various changes in stdlib/examples) and, for me, was more intuitive to use.