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.