Title:   A Tactic Language for the System Coq
Author: David Delahaye

Abstract:

We propose a new tactic language for the system Coq, which is intended to
enrich the current tactic combinators (tacticals). This language is based on a
functional core with recursors and matching operators for Coq terms but also
for proof contexts. It can be used directly in proof scripts or in toplevel
definitions (tactic definitions). We show that the implementation of this
language involves considerable changes in the interpretation of proof scripts,
essentially due to the matching operators. We give some examples which solve
small proof parts locally and some others which deal with non-trivial problems.
Finally, we discuss the status of this meta-language with respect to the Coq
language and the implementation language of Coq.