Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy

mattam82 / Coq-Equations

A function definition package for Coq

http://mattam82.github.io/Coq-Equations

GNU Lesser General Public License v2.1

223 stars 44 forks source link

Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy #566

Closed herbelin closed 10 months ago

herbelin commented 10 months ago

The function create_cbv_infos now needs to know if the reduction is expected to be weak or strong. We set it to strong, preserving the previous semantics.

To be merged synchronously with coq/coq#18190.

SkySkimmer commented 10 months ago

Please merge now