diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/lustrec_mpfr.ml similarity index 100% rename from src/plugins/mpfr/lustrec_mpfr.ml rename to src/lustrec_mpfr.ml diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/lustrec_mpfr.mli similarity index 100% rename from src/plugins/mpfr/lustrec_mpfr.mli rename to src/lustrec_mpfr.mli diff --git a/src/plugins/pluginList.ml b/src/pluginList.ml similarity index 100% rename from src/plugins/pluginList.ml rename to src/pluginList.ml diff --git a/src/plugins/pluginList.mli b/src/pluginList.mli similarity index 100% rename from src/plugins/pluginList.mli rename to src/pluginList.mli diff --git a/src/plugins/pluginType.ml b/src/pluginType.ml similarity index 100% rename from src/plugins/pluginType.ml rename to src/pluginType.ml diff --git a/src/plugins/pluginType.mli b/src/pluginType.mli similarity index 100% rename from src/plugins/pluginType.mli rename to src/pluginType.mli diff --git a/src/plugins/plugins.ml b/src/plugins.ml similarity index 100% rename from src/plugins/plugins.ml rename to src/plugins.ml diff --git a/src/plugins/plugins.mli b/src/plugins.mli similarity index 100% rename from src/plugins/plugins.mli rename to src/plugins.mli