-
Robbert Krebbers authored
This is needed to use coq-stdpp in developments with -type-in-type as set_unfold will otherwise unify with any hyp, causing the set_solver tactic to break.
2aa844c9
This is needed to use coq-stdpp in developments with -type-in-type as set_unfold will otherwise unify with any hyp, causing the set_solver tactic to break.