-
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.
4420aa4d
This change makes it possible to use hlists in the proof mode, which itself uses hlists in the implementation of the specialize tactic.