coq-record-update
coq-record-update copied to clipboard
Add some Ltac to autogenerate Settable
Note that field-setting is up to unification, and so we fully normalize the type of the record when generating the instance. This will be very slow for large record types. Finally, the term generated by setting a field will use unfolded projections, which may be more ugly. The combination of these suggests that you may not want to include this, or you may want to make this optional.