theories/collections.v · 2aa844c9d024e34014b7efb27baa22797b4d079f · Maxime Dénès / stdpp

Forked from Iris / stdpp

Source project has a limited visibility.

7 years ago

Let set_solver/set_unfold only touch Prop hyps. · 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.

2aa844c9

History

Let set_solver/set_unfold only touch Prop hyps.

Robbert Krebbers authored 7 years ago

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.