Fixing issue #6: singleton Prop remain in Prop

CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation

12 stars 3 forks source link

Open herbelin opened 3 years ago

herbelin commented 3 years ago

See #6.

This is on top of the port to 8.13 but it would be easy to adapt to current 8.6-based master (main fix is in 609d11e).