The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

On 22. Apr 2019, at 19:51, Xavier Leroy 
<xavier.leroy AT college-de-france.fr>
 wrote:
> 
> I, too, would like "Opaque" to completely hide the definition of a name, 
> instead of just making it harder to unfold.

I fully agree.  

To give an example, if you want to provide propositional equality but *hide* 
its definition,
you may write

Module Type EQ.
  Parameter eq : forall X, X -> X -> Prop.
  Parameter Q : forall X x, eq X x x.
  Parameter R : forall X x y (p: X -> Prop), eq X x y -> p x -> p y.
End EQ.

Module EqLeibniz : EQ.
  Definition eq X x y := forall p: X -> Prop, p x -> p y.
  Definition Q X x : eq X x x := fun p h => h.
  Definition R X x y p (f: eq X x y) := f p.
End EqLeibniz.

Open EqLeibniz.

With a real “Opaque” you could just write

Definition eq X x y := forall p: X -> Prop, p x -> p y.
Definition Q X x : eq X x x := fun p h => h.
Definition R X x y p (f: eq X x y) := f p.
Opaque eq Q R.

Much easier to explain to students who don’t know ML modules.

Gert