The Coq mailing list

[Nico <nlehmann AT dcc.uchile.cl>]

Hi all,

I want to write a plugin that expose a type that can be introduced only by a ocaml tactic that check if the parameters of the type satisfies a structural constraint regarding the axioms on which it relies.

If I hide the implementation of the type using type modules I cannot access the type constructor on the tactic, and thus cannot introduce the type.

Is there a way in which I can access a member not exposed in the module type through a ocaml tactic?

Thanks