From 5db591257070734439dd5550995d6d3f497256c0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 22 Mar 2019 06:33:49 +0100 Subject: [dune] [stdlib] Build the standard library natively with Dune. This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility? --- plugins/ssr/dune | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 plugins/ssr/dune (limited to 'plugins/ssr/dune') diff --git a/plugins/ssr/dune b/plugins/ssr/dune new file mode 100644 index 0000000000..a117d09a16 --- /dev/null +++ b/plugins/ssr/dune @@ -0,0 +1,9 @@ +(library + (name ssreflect_plugin) + (public_name coq.plugins.ssreflect) + (synopsis "Coq's ssreflect plugin") + (modules_without_implementation ssrast) + (flags :standard -open Gramlib) + (libraries coq.plugins.ssrmatching)) + +(coq.pp (modules ssrvernac ssrparser)) -- cgit v1.2.3