Rtac – a reflective tactic language for Coq. Computational reflection is a useful technique for avoiding the overhead inherent in constructing large proof objects. However, to date it is significantly more time consuming to write reflective procedures than the equivalent tactics. Can we build a lightweight tactic language for building reflective procedures easily? To this end, we present Rtac, a lightweight, work-in-progress, tactic language built on top of MirrorCore, a parametric framework for writing reflective decision procedures in Coq