Elpi Query lp:{{
 std.do! [
   coq.env.begin-module-type "TF" [],
     coq.env.add-axiom "w" {{nat}} _,
   coq.env.end-module-type MP_TF,
   coq.locate-module-type "TA" MP_TA,
   coq.env.begin-module "F" (some MP_TF) [pr "a" MP_TA, pr "b" MP_TA],
   coq.env.import-module {coq.locate-module "a"},
   coq.env.add-const "w" {{z}} _ _ _, %<-- This fails unexpectedly ("z not found").
   coq.env.end-module _
 ]
}}.
Print F.
Module B := F A A.
Print B.
Print B.w.

   coq.env.begin-module-type "TA" [],
     coq.env.add-axiom "z" {{nat}} _,
     coq.env.add-axiom "i" {{Type}} _,
   coq.env.end-module-type MP_TA,

  (* XXX When Coq's API allows it, call vernacentries directly *)
  MLCode(Pred("coq.env.begin-module",
    In(id, "Name",
    In(option modtypath, "ModTyPath",
    In(list (pair id modtypath), "Functor arguments",
    Full(unit_ctx, "Starts a module, the modtype can be omitted *E*")))),
  (fun name mp binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module" (fun state ->
     if Global.sections_are_opened () then
       err Pp.(str"This elpi code cannot be run within a section since it opens a module");
     let ty =
       match mp with
       | None -> Declaremods.Check []
       | Some mp ->
           let fpath = Nametab.path_of_modtype mp in
           let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
           Declaremods.(Enforce (CAst.make tname, DefaultInline)) in
     let id = Id.of_string name in
     let binders_ast =
       List.map (fun (farg_id,farg_mp) ->
           let fpath = Nametab.path_of_modtype farg_mp in
           let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
           [CAst.make (Id.of_string farg_id)], (CAst.make tname, Declaremods.DefaultInline))
         binders_ast in
     let _mp = Declaremods.start_module None id binders_ast ty in
     state, (), []))),
  DocAbove);