The core API makes it possible to register a `valexpr` for each
`ltac_constant`.

For functional `ltac_constant` (the vast majority) this will be a
closure, which in valexpr are represented as arbitrary OCaml closures.
This allows arbitrary compilation schemes, eg
- dynlinked OCaml code as in
  https://github.com/coq/coq/pull/17521 (like native_compute)
- compiling to the VM eg
  `let code = compile expr in mk_closure arity (fun args -> interpret code args)`
- partially evaluating the tacexpr and sending it back to the normal evaluator
  `let e = partial_eval e in mk_closure arity (fun args -> interp (TacApp (e, args))`

and any other scheme someone might come up with.

We also expose some convenient APIs.