Module Rewrite

module Rewrite: sig .. end
Definition of the tactics, and corresponding Coq grammar entries.