search

coq-community / paramcoq

Coq plugin for parametricity [maintainer=@proux01]
Other
44 stars 24 forks source link

Adapt to Coq PR #14846: references to inductive types in the type of constructors are directly Ind rather than Rel nodes #77

Closed herbelin closed 3 years ago

herbelin commented 3 years ago

We insert a translation function which emulates the previous behavior. Note also that subst_instance_constr now needs a disambiguation.

This is to be merged synchronously with coq/coq#14846.

Note: In passing, and independently, we adapt to a warning (lift_rel_context now provided by Coq).