Re: How to use the nested module in OCaml object files

Ok, i've solved this problem... the source i read is the latest but the Coq
i used is 8.5. the source has some changes.

2016-04-22 14:53 GMT+08:00 Zhang Hengruo [email protected]
[ocaml_beginners] <[email protected]>:

>
>
> Hi all,
>
> I'm writing a Coq plugin and I need some functions in Coq source. For
> example,
>
> module Named :sig
>    module Declaration :
>    sig
>       type t = LocalAssum of Id.t * Constr.t
>              | LocalDef of Id.t * Constr.t * Constr.t
>       ...
>    end
>    ...end
>
> This module is in kernel/context.ml. I want use the constructor
> LocalAssum and LocalDef to parse something, but I can't use them. It seems
> that the .cmi and .cma file in $COQLIB only expose the members in
> context.ml but not the ones in nested modules. I've tried adding open
> Context.Named.Declaration but compiler told me "Error: Unbound module
> Context.Named".
>
> Any help appreciated.
>
> Thanks, Hengruo
>
> 
>