Skip to content

Remove the existentials from top-level modules

Guillaume Claret requested to merge remove-existentials into master

In this MR we remove the existential types from the records of the top-level modules. This should help proving properties about modules and functors.

Merge request reports