With advice from Greg, I've been trying to stage Coq's Ltac language.
The first barrier, of course, being to compile the damn thing... This patch gets that working.
The biggest issue is that MetaOCaml's runtime includes the OCaml
compiler, exposing a lot of the compiler's internal modules: Closure,
Match, etc. Unfortunately, many of these clash with Coq modules with the same names. The patch solves this problem by packing all the modules into a single
module named Metanative (maybe it should be Metalib or Metaocaml or
something, but whatever), and forcing all accesses to the runtime
compiler to go through this wrapper module.
Right now this scheme gets metaocamlopt working more or less as
before, except that code referring to Trx needs to open Metanative or
replace Trx with Metanative.Trx. None of the compiler modules are
exposed directly, so the clashes are resolved and Coq compiles
successfully.
In byte code, most modules are again packed into Metanative, but both
the byte code compiler and toplevel (metaocamlc and metaocaml, resp)
exposes Trx. The byte code utilities link with toplevellib, which
imports and therefore exposes Trx. This dependence seems to be hard
to remove: toplevellib is where the code lives that type checks and
executes ASTs constructed at runtime.
