<div dir="ltr"><div><div><div><div><div><div><div><div><div><div><div><div><div><div><div><div>If the module is a record, we use<br></div><br>"open Pair p"<br><br></div>If it is a simple module<br><br></div>"open B"<br><br></div>if it is a parametrized module<br><br></div>"module C = B a<br></div> open C"<br><br></div>or <br><br></div>"open module C = B a"<br><br><br></div>I find that all these different ways to open a module complicate things.<br></div>I would prefer if there was a single concept and that reflected into a uniform way of opening a module.<br><br></div>For example, every module is a record.<br></div>A parametrized module is a parametrized record.<br><br></div>And omit "Pair". Just write:<br></div>"open p"<br><br></div>or <br><br></div>"open (p a)". <br></div>