Unfold 'constructor' more aggressively

tchajed / coq-record-update

Library to create Coq record update functions

MIT License

42 stars 16 forks source link

Unfold 'constructor' more aggressively #8

Closed jakobbotsch closed 4 years ago

jakobbotsch commented 5 years ago

In proofs I often see constructor x y in my goal which I need to manually unfold to get x. This change makes cbn and simpl unfold it automatically.

tchajed commented 4 years ago

This looks good, thanks!