A term derived from Coq's usage of it meaning a program which operates on a declarative system in a procedural manner. That is, it operates on the declarative system in the mode of directing the proof of it, possibly re-using existing proof procedures or overriding default ones.

This can be compared and contrasted with Maude's rewrite logic strategies.

This page is linked from: Coq   Yarrow