diff options
| author | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
| commit | 7602c2cb547fe6664f7a065d17717baf12b9da88 (patch) | |
| tree | 1b034b3646090d35a8d730cbec6a5cf1c91da804 /user-contrib/Ltac2/plugin_base.dune | |
| parent | 8aa64e7c4661549fef63a1c9c2e4e5284db911d8 (diff) | |
| parent | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (diff) | |
Merge PR #10002: Integrate ltac2
Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'user-contrib/Ltac2/plugin_base.dune')
| -rw-r--r-- | user-contrib/Ltac2/plugin_base.dune | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/plugin_base.dune b/user-contrib/Ltac2/plugin_base.dune new file mode 100644 index 0000000000..711e9b95d3 --- /dev/null +++ b/user-contrib/Ltac2/plugin_base.dune @@ -0,0 +1,6 @@ +(library + (name ltac2_plugin) + (public_name coq.plugins.ltac2) + (synopsis "Coq's Ltac2 plugin") + (modules_without_implementation tac2expr tac2qexpr tac2types) + (libraries coq.plugins.ltac)) |