-
Robbert Krebbers authored
This change makes it possible to use hlists in the proof mode, which itself uses hlists in the implementation of the specialize tactic.
ae3c8fdf
This change makes it possible to use hlists in the proof mode, which itself uses hlists in the implementation of the specialize tactic.