The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi Coq-clubbers,

When going through the standard library, I often find Hints declared
in Module signatures, like FSetInterface.S ... So, in order to get
these Hints, it seems that I must enforce the output module type of
FSetAVL.Make to meet this interface. But, the latter solution prevents
the unfolding of all symbols (like, e.g. all the computation
functions), and it seems a little bit tedious to export everything
useful.

Is there another solution to get the Hints, and keep everything transparent ?

Here is a code sample that summarizes what I have tried ...
<<
Require Import FSets.

Module NatSet := FSetList.Make(Nat_as_OT).
Check (O : NatSet.elt).
(* Print HintDb set. No such Hint database *)

Module NatSetChecked <: FSetInterface.S := FSetList.Make(Nat_as_OT).
Check (O : NatSetChecked.elt).
(* Print HintDb set. No such Hint database *)

Module NatSetCoerced : FSetInterface.S := FSetList.Make(Nat_as_OT).
(* Check (O : NatSetCoerced.elt).   NatSetCoerced.elt is opaque *)
 Print HintDb set. (* Here I get all the hints I want *)

Module NatSetCoerced2 : FSetInterface.S with Module E := Nat_as_OT :=
FSetList.Make(Nat_as_OT).
Check (O : NatSetCoerced2.elt).  (* OK *)
Print HintDb set. (* Here I get all the hints I want *)
Eval vm_compute in (NatSetCoerced2.exists_ (fun u => if le_lt_dec 0 u
then true else false) NatSetCoerced2.empty). (* NatSetCoerced2.empty
is opaque *)

>>

-- 
thomas