Name		Name	Last commit message	Last commit date
parent directory ..
META.coq-elpi		META.coq-elpi
README.md		README.md
coq_elpi_HOAS.ml		coq_elpi_HOAS.ml
coq_elpi_HOAS.mli		coq_elpi_HOAS.mli
coq_elpi_arg_HOAS.ml		coq_elpi_arg_HOAS.ml
coq_elpi_arg_HOAS.mli		coq_elpi_arg_HOAS.mli
coq_elpi_arg_syntax.mlg		coq_elpi_arg_syntax.mlg
coq_elpi_builtins.ml		coq_elpi_builtins.ml
coq_elpi_builtins.mli		coq_elpi_builtins.mli
coq_elpi_builtins_synterp.ml		coq_elpi_builtins_synterp.ml
coq_elpi_builtins_synterp.mli		coq_elpi_builtins_synterp.mli
coq_elpi_glob_quotation.ml		coq_elpi_glob_quotation.ml
coq_elpi_glob_quotation.mli		coq_elpi_glob_quotation.mli
coq_elpi_graph.ml		coq_elpi_graph.ml
coq_elpi_graph.mli		coq_elpi_graph.mli
coq_elpi_name_quotation.ml		coq_elpi_name_quotation.ml
coq_elpi_programs.ml		coq_elpi_programs.ml
coq_elpi_programs.mli		coq_elpi_programs.mli
coq_elpi_utils.ml		coq_elpi_utils.ml
coq_elpi_utils.mli		coq_elpi_utils.mli
coq_elpi_vernacular.ml		coq_elpi_vernacular.ml
coq_elpi_vernacular.mli		coq_elpi_vernacular.mli
coq_elpi_vernacular_syntax.mlg		coq_elpi_vernacular_syntax.mlg
dune		dune
elpi_plugin.mlpack		elpi_plugin.mlpack

README.md

Coq Elpi plugin

This directory contains the OCaml code bridging Elpi and Coq.

The most interesting file is coq_elpi_HOAS.ml where conversions for term, context and evar_map are provided.

The exposed Coq API is in coq_elpi_builtins.ml.