diff --git a/.gitignore b/.gitignore
index 2174e4d2804d3239c06a6c1133e0f3aea38a85df..938cbaf4aa62fe41538c440a32d370f4d6a790b0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,10 +1,8 @@
 *~
+_build/
 /src/_build/
 /setup.data
 /setup.log
-/src/version.ml
-/src/pluginList.ml
-/myocamlbuild.ml
 *.cmt
 *.log
 Makefile
@@ -12,4 +10,4 @@ Makefile
 /src/_tags
 /bin
 *cache/
-/config.status
\ No newline at end of file
+/config.status
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 0000000000000000000000000000000000000000..76c0584257f0812ce6801d34316523d14ea00b24
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,346 @@
+# This reusable CI script is licensed under the MIT license.
+# See the complete license text at the end.
+
+### Configuration section
+
+# The versions of the compiler to test the project against.
+.build-matrix:
+  parallel:
+    # https://docs.gitlab.com/ee/ci/yaml/README.html#parallel-matrix-jobs
+    matrix:
+    # - OCAML_COMPILER: "4.00.1"
+    # - OCAML_COMPILER: "4.01.0"
+    # - OCAML_COMPILER: "4.02.1"
+    # - OCAML_COMPILER: "4.02.3"
+    # - OCAML_COMPILER: "4.03.0"
+    # - OCAML_COMPILER: "4.04.2"
+    # - OCAML_COMPILER: "4.05.0"
+    # - OCAML_COMPILER: "4.06.1"
+    # - OCAML_COMPILER: "4.07.1"
+    # - OCAML_COMPILER: "4.08.1"
+    # - OCAML_COMPILER: "4.09.1"
+    # - OCAML_COMPILER: "4.10.0"
+    - OCAML_COMPILER: "4.11.1"
+
+variables:
+  CLEAN_OPAM_CACHE: "false"
+  CLEAN_DUNE_CACHE: "false"
+  # If CLEAN_OPAM_CACHE is set to "true", the opam switch from previous CI jobs
+  # will not be reused.
+  # If CLEAN_DUNE_CACHE is set to "true", the dune _build directory
+  # from previous CI jobs will not be reused.
+
+  # In particular, you can run a manual pipeline
+  # with either variable set to "true" to purge a faulty cache.
+
+  # To run a manual gitlab pipeline, on your project go to
+  # "CI/CD" > pipelines, click "Run pipeline", the interface
+  # then offers to override variables, so you can change the
+  # value of any variable defined here.
+
+  DUNE_BUILD_TARGETS: "@all"
+  DUNE_TEST_TARGETS: "@runtest"
+  DUNE_DOC_TARGETS: "@doc"
+  # If you make one of these variables empty (: ""),
+  # the corresponding build step will be skipped.
+  # Setting them to other values can refine the build
+  # process, for example "@foo/runtest @bar/runtest" would only
+  # run the tests inside directories 'foo/' and 'bar/'
+  # (see Dune documentation on target aliases).
+
+
+# This CI script is written to be portable across projects.
+# None of the code below hardcodes project filenames,
+# OCaml versions or other project-specific details.
+#
+# If you want to add new behavior for your project, we recommend
+# trying to factorize it with project-agnostic code below,
+# and project-specific or manually-overridable choices in the
+# 'variables' section above.
+
+
+### Hacking advice
+#
+# Reference documentation for Gitlab CI configuration files:
+#  https://docs.gitlab.com/ee/ci/yaml/
+#
+# If you edit this file and make syntax errors, the default
+# error messages will not help you, but Gitlab offers a "CI Lint"
+# service that provides very nice error messages:
+#   https://docs.gitlab.com/ee/ci/lint.html
+#
+# To use this linter, go to "CI/CD > Pipelines", click the "CI Lint"
+# button in the top right, copy-paste your .gitlab-ci.yml file in
+# the form and click "Validate".
+#
+# We recommend systematically using the CI Lint whenever you change
+# this file, it can save you from wasted time and frustration.
+
+
+### Stages
+
+stages:
+  - build        # build the project and run its tests
+  - deploy       # deploys a website to Pages from the 'pages' branch
+
+
+### Build stage
+#
+# build the project and run its tests
+
+build:
+  stage: build
+
+  extends: .build-matrix # defines OCAML_COMPILER
+
+  variables:
+    ARTIFACTS: "artifacts/$OCAML_COMPILER"
+    # a local shortcut for the per-compiler artifact repository
+
+    FF_USE_FASTZIP: "true"
+    # A workaround against a bug in gitlab-runner's default
+    # unzipping implementation, which partially breaks caching for the dune _build cache.
+    # See https://gitlab.com/gitlab-org/gitlab-runner/-/issues/27496 for more details.
+
+  artifacts:
+    paths:
+      - artifacts/$OCAML_COMPILER
+
+  # run this job only if a 'dune-project' file exists;
+  # (In particular, this will not run in your "pages" branch
+  # if it does not itself use Dune.)
+  rules:
+    # https://docs.gitlab.com/ee/ci/yaml/#rules
+    - exists:
+        - dune-project
+
+  # This CI script uses a local switch, so we don't need
+  # a docker image with a pre-installed OCaml version, just opam.
+  # See https://hub.docker.com/r/ocaml/opam/ for other images.
+  image: ocaml/opam:debian-testing-opam
+
+  # We use a local opam switch in `./_opam` that is cached
+  # by Gitlab, and reused across all branches and pull requests.
+  cache:
+    # https://docs.gitlab.com/ee/ci/yaml/#cache
+    key: $OCAML_COMPILER
+    # keep a distinct cache for each compiler version
+    paths:
+      - _opam
+      # Reusing the same opam environment over a long time might result into
+      # unnatural choice of dependencies: repeatedly installing and updating
+      # dependencies may result in a different solver choices than doing
+      # a fresh setup.
+      #
+      # You can manually clean the _opam cache by running a manual pipeline
+      # with the variable CLEAN_OPAM_CACHE set to "true".
+
+      - _build
+      # You can manually clean the dune _build cache by running a manual pipeline
+      # with the variable CLEAN_DUNE_CACHE set to "true".
+
+  script:
+    - if [ "$CLEAN_OPAM_CACHE" == "true" ]; then echo "we clean the _opam cache as explicitly requested"; rm -fR _opam; fi
+    - if [ "$CLEAN_DUNE_CACHE" == "true" ]; then echo "we clean the dune _build cache as explicitly requested"; rm -fR _build; fi
+    # Note: Gitlab supports multi-line scripts with "- |" or "- >", but the
+    # display in the logs does not show the whole script being run, reducing
+    # understandability. We only use multi-line scripts for "echo" line,
+    # and otherwise keep long one-liners.
+    #   https://docs.gitlab.com/ee/ci/yaml/script.html#split-long-commands
+
+    # see https://docs.gitlab.com/ee/ci/jobs/index.html#custom-collapsible-sections
+    # to understand the "section_{start,end}:`date +%s`:<name>\r\e[0K human-readable text" pattern
+    - echo -e "section_start:`date +%s`:setup_switch\r\e[0K setup opam switch"
+    - if [ -d _opam ]; then echo "we reuse the local opam switch from the CI cache"; fi
+
+    - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . $OCAML_COMPILER; fi
+    # --no-install prevents installing the package or its dependencies.
+    # we want to setup the external dependencies (depext) first, see below.
+    - echo -e "section_end:`date +%s`:setup_switch\r\e[0K"
+
+    - echo -e "section_start:`date +%s`:setup_deps\r\e[0K setup the package dependencies"
+    # (Note: when opam 2.1 will be available with native depext integration,
+    # the complex dance below will be replaceable by just
+    #   opam install . --deps-only --locked --with-test --with-doc --yes
+    # which should start by installing depexts
+    # (possibly we will need to set some explicit environment variable first).
+    - opam install depext --yes
+    - opam install . --dry-run --deps-only --locked --with-test --with-doc --yes | awk '/-> installed/{print $3}' | xargs opam depext -iy
+    # the magical command above comes from https://github.com/ocaml/opam/issues/3790
+    # it installs both external dependencies and opam dependencies
+    - echo "(we used --locked to honor any lockfiles if present)"
+    - echo -e "section_end:`date +%s`:setup_deps\r\e[0K"
+
+    - echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
+    - eval $(opam env)
+    - if [ "$DUNE_BUILD_TARGETS" != "" ]; then dune build $DUNE_BUILD_TARGETS --display short; else echo "skipped (DUNE_BUILD_TARGETS is empty)"; fi
+    - echo -e "section_end:`date +%s`:project_build\r\e[0K"
+
+    - echo -e "section_start:`date +%s`:project_tests\r\e[0K run the tests"
+    - if [ "$DUNE_TEST_TARGETS" != "" ]; then dune build $DUNE_TEST_TARGETS --display short; else echo "skipped (DUNE_TEST_TARGETS is empty)"; fi
+    - echo -e "section_end:`date +%s`:project_tests\r\e[0K"
+
+    - echo -e "section_start:`date +%s`:project_doc\r\e[0K build the documentation"
+    - if [ "$DUNE_DOC_TARGETS" != "" ]; then dune build $DUNE_DOC_TARGETS --display short; else echo "skipped (DUNE_DOC_TARGETS is empty)"; fi
+    - echo -e "section_end:`date +%s`:project_doc\r\e[0K"
+
+    - echo -e "section_start:`date +%s`:artifacts\r\e[0K populating the artifacts"
+    - mkdir -p $ARTIFACTS
+    - >
+      echo "Build artifacts will be available at
+              $CI_JOB_URL/artifacts/browse/$ARTIFACTS
+            Note: by default Gitlab only keeps them for a few weeks."
+    - >
+      if [ "Dune_DOC_TARGETS" != "" ]; then
+        cp -r _build/default/_doc/_html $ARTIFACTS/doc;
+        echo "Documentation:
+              $CI_JOB_URL/artifacts/browse/$ARTIFACTS/doc/index.html";
+      fi
+    - >
+      if [ -f _build/log ];
+      then
+        mkdir -p $ARTIFACTS/_build;
+        cp _build/log $ARTIFACTS/_build/log
+        echo "Dune build log:
+              $CI_JOB_URL/artifacts/browse/$ARTIFACTS/_build/log";
+      fi
+    - echo -e "section_end:`date +%s`:artifacts\r\e[0K"
+
+
+### CI performance
+
+# Performance analysis of one 'build' job on a small, simple library project
+# (the project build/test/doc time is basically neglectible) on gitlab.com:
+#
+# (To get those numbers for your project, just look at a passing build and fold all
+#  log sections.)
+#
+# 2m total
+#   56s preparing the docker image and CI environment
+#   14s restoring the _opam cache
+#   10s installing the project dependencies
+#       (external dependencies are not cached, opam dependencies are cached)
+#    3s project build, tests, doc
+#   31s saving the _opam cache
+#    6s uploading artifacts
+#
+# When running with CLEAN_OPAM_CACHE=true, the costs are similar, except for
+#  7m30s building the local opam switch
+#  2m07s building the project dependencies (external and opam)
+# This shows that caching the local _opam switch is very important, as
+# its setup time dominates the build (for a small project).
+#
+# Another thing that is clear from these numbers is that splitting
+# your CI in several jobs could be fairly expensive: for each job you
+# pay 56s seconds of docker setup, plus 14s to restore the _opam
+# cache. (The 31s to save the cache afterwards can be avoided by using
+# a "policy: pull" setting if the job uses the _opam in a read-only
+# way.)
+#
+# This is why this CI script does everything in a single 'build' step.
+
+
+### Deploy stage
+#
+# pushing some project artifacts to the web.
+
+# The "pages" rule uploads a custom website whenever someones
+# pushes a commit to the "pages" branch of the repository.
+#
+# The content of the website is the sub-filesystem
+# located in the "docs/" subdirectory of the branch index.
+#
+# This behavior emulates the way per-repository Github pages work.
+#
+# If the repository is at
+#   https://gitlab.com/<group>/<project>,
+# then the published website will be at
+#   https://<group>.gitlab.io/<project>
+# In general see
+#   https://docs.gitlab.com/ee/user/project/pages/getting_started_part_one.html#gitlab-pages-default-domain-names
+#
+# We previously used a setup where the documentation was pushed to
+# Gitlab Pages automatically when pushing a tag (a new release). This
+# was much less flexible, with no easy way for users to publish web
+# content *other* than the documentation, or to control when the
+# content should be refreshed.
+#
+# It is fairly simple to publish the documentation
+# from any branch with the current interface.
+# Here is an example script:
+#
+#    # compute the current commit hash and branch name
+#    git rev-parse --short HEAD > /tmp/commit
+#    git rev-parse --abbrev-ref HEAD > /tmp/branch
+#    cat .gitlab-ci.yml /tmp
+#
+#    # move to the 'pages' branch and commit the documentation there
+#    git checkout pages
+#    mkdir -p docs
+#    git rm --ignore-unmatch -r docs > /dev/null
+#    cp -r ${DOC_PATH} docs
+#    git add docs
+#    # we ensure that the CI configuration is present on the 'pages' branch,
+#    # otherwise pushing from there may not deploy as expected.
+#    cp /tmp/.gitlab-ci.yml .
+#    git add .gitlab-ci.yml
+#    git commit -m "documentation for $(cat /tmp/branch) ($(cat /tmp/commit))" \
+#    && git checkout $(cat /tmp/branch) \
+#    || git checkout $(cat /tmp/branch)
+#
+#    echo
+#    echo "The documentation was committed to the 'pages' branch."
+#    echo "You can now push it with"
+#    echo "    git push origin pages"
+#
+pages:
+  # Hardcoded values in the job:
+  # (for Gitlab to understand that this job builds the Pages)
+  # - the job name must be 'pages'
+  # - the stage must be 'deploy'
+  # - the artifacts must be a 'public' directory
+
+  stage: deploy
+
+  # no need for an OCaml environment
+  image: alpine:latest
+
+  # no cache
+
+  # run this job only in the 'pages' branch
+  rules:
+    # https://docs.gitlab.com/ee/ci/yaml/#rules
+    - if: '$CI_COMMIT_REF_NAME == "pages"'
+      when: on_success
+  artifacts:
+    paths:
+      - public
+  script:
+    - rm -fR public/
+    - mkdir -p docs
+    - cp -r docs public
+
+
+
+## MIT License
+#
+# Copyright 2021 Gabriel Scherer
+#
+# Permission is hereby granted, free of charge, to any person obtaining
+# a copy of this software and associated documentation files
+# (the "Software"), to deal in the Software without restriction,
+# including without limitation the rights to use, copy, modify, merge,
+# publish, distribute, sublicense, and/or sell copies of the Software,
+# and to permit persons to whom the Software is furnished to do so,
+# subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be
+# included in all copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+# LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+# OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+# WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/.merlin b/.merlin
deleted file mode 100644
index 1a23de0d48d69f367b19309a0b102cc15f08f50f..0000000000000000000000000000000000000000
--- a/.merlin
+++ /dev/null
@@ -1,43 +0,0 @@
-S src
-S src/backends
-S src/backends/C
-S src/backends/EMF
-S src/backends/Horn
-S src/backends/Java
-S src/checks
-S src/features
-S src/features/machine_types
-S src/parsers
-S src/plugins
-S src/plugins/mpfr
-S src/plugins/salsa
-S src/plugins/scopes
-S src/tools
-S src/tools/stateflow
-S src/tools/stateflow/common
-S src/tools/stateflow/json-parser
-S src/tools/stateflow/models
-S src/tools/stateflow/semantics
-S src/utils
-
-B src/_build
-B src/_build/backends
-B src/_build/backends/C
-B src/_build/backends/EMF
-B src/_build/backends/Horn
-B src/_build/checks
-B src/_build/features
-B src/_build/features/machine_types
-B src/_build/parsers
-B src/_build/plugins
-B src/_build/plugins/mpfr
-B src/_build/plugins/salsa
-B src/_build/plugins/scopes
-B src/_build/tools
-B src/_build/tools/stateflow
-B src/_build/tools/stateflow/common
-B src/_build/tools/stateflow/models
-B src/_build/tools/stateflow/semantics
-B src/_build/utils
-
-B test
diff --git a/README.md b/README.md
index f6ee55c5c79dbc86d8da608bd02875cc97c99fe1..9c81bfb23f8a63969e88f6bb6d67b87609af45e7 100644
--- a/README.md
+++ b/README.md
@@ -10,14 +10,22 @@ LustreC is a modular compiler of Lustre code into C and Horn Clauses.
 
 # Dependencies
 On a fresh ubuntu/debian-like install
-> apt-get install opam libmpfr-dev
+ ```
+ apt-get install opam libmpfr-dev
+ ```
 Get a fresh version of ocaml
-> opam switch 4.06.1
+ ```
+opam switch create 4.06.1
+ ```
 Install some dependencies
-> opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
+ ```
+opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
+ ```
 In OSX, some issues with Z3, please pin the following version:
-> opam pin add z3 4.8.1
-> opam install z3
+ ```
+opam pin add z3 4.8.1
+opam install z3
+ ```
 # Build
 ```
 > autoconf
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..8bd223080bf86acce3a6ad9121a31adce85053b8
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,32 @@
+(lang dune 2.8)
+(name lustrec)
+(version 1.7)
+
+(using dune_site 0.1)
+(using menhir 2.0)
+(generate_opam_files true)
+
+(license LGPL)
+(authors "Pierre-Loic Garoche <ploc@garoche.net>"
+         "Xavier Thirioux <thirioux@enseeiht.fr>")
+(maintainers "Pierre-Loic Garoche <ploc@garoche.net>")
+(source (uri git+https://cavale.enseeiht.fr/git/lustrec#unstable))
+(bug_reports https://cavale.enseeiht.fr/redmine/projects/lustrec/issues)
+(homepage https://cavale.enseeiht.fr/redmine/projects/lustrec/)
+
+(package
+ (name lustrec)
+ (sites
+  (lib plugins)
+  (lib verifiers))
+ (synopsis "A Lustre compiler toolset")
+ (description
+   "lustrec is structured around the modular compilation scheme proposed by \
+    Biernacki, Colaço, Hamon, and Pouzet at LCTES'08.  It is an open source \
+    lustre compiler that provides verification capabilities. It is currently \
+    mainly used through the CocoSim platform, a Matlab toolbox to perform V&V \
+    of Simulink models. Within CocoSim, the Lustre language is used as an \
+    intermediate representation and relies mainly on lustrec to produce code \
+    or verification artifacts.")
+ (depends ocamlgraph menhir conf-mpfr)
+ (depopts z3 yojson))
diff --git a/lustrec.opam b/lustrec.opam
new file mode 100644
index 0000000000000000000000000000000000000000..5b331bac22e453c9a9d6bae2fa6658b2f34f2ca6
--- /dev/null
+++ b/lustrec.opam
@@ -0,0 +1,33 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "1.7"
+synopsis: "A Lustre compiler toolset"
+description:
+  "lustrec is structured around the modular compilation scheme proposed by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08.  It is an open source lustre compiler that provides verification capabilities. It is currently mainly used through the CocoSim platform, a Matlab toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre language is used as an intermediate representation and relies mainly on lustrec to produce code or verification artifacts."
+maintainer: ["Pierre-Loic Garoche <ploc@garoche.net>"]
+authors: [
+  "Pierre-Loic Garoche <ploc@garoche.net>"
+  "Xavier Thirioux <thirioux@enseeiht.fr>"
+]
+license: "LGPL"
+homepage: "https://cavale.enseeiht.fr/redmine/projects/lustrec/"
+bug-reports: "https://cavale.enseeiht.fr/redmine/projects/lustrec/issues"
+depends: [
+  "dune" {>= "2.8"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
diff --git a/opam b/opam
deleted file mode 100644
index 093cbb769cd741efef3a0d72f210931e671fd3de..0000000000000000000000000000000000000000
--- a/opam
+++ /dev/null
@@ -1,44 +0,0 @@
-opam-version: "2.0"
-name: "lustrec"
-version: "1.7"
-maintainer: "Pierre-Loic Garoche <ploc@garoche.net>"
-authors: ["Pierre-Loic Garoche <ploc@garoche.net>" "Xavier Thirioux <thirioux@enseeiht.fr>"]
-homepage: "https://cavale.enseeiht.fr/redmine/projects/lustrec/"
-bug-reports: "https://cavale.enseeiht.fr/redmine/projects/lustrec/issues"
-license: "LGPL"
-dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
-build: [
-  ["autoconf"]
-  ["./configure" "--prefix=%{prefix}%"]
-  [make]
-]
-install: [make "install"]
-remove: [make "uninstall"]
-depends: [
-  "ocamlfind"
-  "yojson"
-  "cmdliner"
-  "fmt"
-  "ppx_deriving_yojson"
-  "ppx_traverse_builtins"
-  "ppxlib"
-  "menhir"
-  "ocamlgraph"
-  "logs"
-  "z3"
-  "num"
-]
-synopsis: "A Lustre compiler toolset"
-description: """
-lustrec is structured around the modular compilation scheme proposed
-by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08.  It is an open
-source lustre compiler that provides verification capabilities.
-It is currently mainly used through the CocoSim platform, a Matlab
-toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre
-language is used as an intermediate representation and relies mainly
-on lustrec to produce code or verification artifacts.
-"""
-url {
-  src: "https://cavale.enseeiht.fr/redmine/attachments/download/117/lustrec-1.6-Xia-Zhu-src.tgz"
-  checksum: "md5=f06e87d5fbb24c91894bdc55bf6cc496"
-}
diff --git a/src/.merlin b/src/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/arrow.ml b/src/arrow.ml
index 1ce3b268e1843be36510f033dbe97af8de1980e9..610b47929060ca38037250f69d350e2fa9c65362 100644
--- a/src/arrow.ml
+++ b/src/arrow.ml
@@ -23,7 +23,7 @@ let arrow_desc =
     node_iscontract = false;
 }
 
-let arrow_top_decl =
+let arrow_top_decl () =
   {
     top_decl_desc = Node arrow_desc;
     top_decl_owner = (Options_management.core_dependency "arrow");
diff --git a/src/arrow.mli b/src/arrow.mli
index ae329a1bffd7f13d98f3b50833758b8afe3ddca4..ace9a2854f67adef232de96efcc3910cab9dc39b 100644
--- a/src/arrow.mli
+++ b/src/arrow.mli
@@ -1,3 +1,3 @@
 val arrow_id: string
-val arrow_top_decl: Lustre_types.top_decl
+val arrow_top_decl: unit -> Lustre_types.top_decl
 val arrow_desc: Lustre_types.node_desc
diff --git a/src/backends/.merlin b/src/backends/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Ada/.merlin b/src/backends/Ada/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/Ada/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/C/.merlin b/src/backends/C/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/C/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index fb1d06a1ba5a3aefb799351a88e486489159b353..cff0245a2f018ef5651fdc48b78f4ec1ad53c4de 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -45,9 +45,9 @@ let print_import_standard fmt =
 	fprintf fmt "#include <mpfr.h>@."
       end;
     if !Options.cpp then
-      fprintf fmt "#include \"%s/arrow.hpp\"@.@." Arrow.arrow_top_decl.top_decl_owner 
+      fprintf fmt "#include \"%s/arrow.hpp\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
     else
-      fprintf fmt "#include \"%s/arrow.h\"@.@." Arrow.arrow_top_decl.top_decl_owner 
+      fprintf fmt "#include \"%s/arrow.h\"@.@." (Arrow.arrow_top_decl ()).top_decl_owner
 	
   end
 
diff --git a/src/backends/EMF/.merlin b/src/backends/EMF/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/EMF/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Horn/.merlin b/src/backends/Horn/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/Horn/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/backends/Java/.merlin b/src/backends/Java/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/backends/Java/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/checks/.merlin b/src/checks/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/checks/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/checks/liveness.ml b/src/checks/liveness.ml
index dd6c48aa32c4e8a91f4e2349d923b1fc102372bb..542344b38bbb739a6f9af7783edcd27525704034 100644
--- a/src/checks/liveness.ml
+++ b/src/checks/liveness.ml
@@ -12,7 +12,6 @@
 open Utils
 open Lustre_types
 open Corelang
-open Graph
 open Causality
 
 type context =
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000000000000000000000000000000000000..8690c7da4a1c90b15139ad3c03da4c9261922077
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,128 @@
+(env
+ (dev
+  (flags (:standard -warn-error -A))))
+
+(include_subdirs unqualified)
+
+(library
+ (name lustrec_interface)
+ (package lustrec)
+ (modules
+   lustre_types
+   utils
+   lustre_utils
+   location
+   dimension
+   env
+   real
+   types
+   options
+   version
+   clocks
+   delay
+   machine_code_types
+   scheduling_type
+   log
+   printers
+   corelang
+   basic_library
+   type_predef
+   clock_predef
+   delay_predef
+   error
+   global
+   annotations
+   machine_code_common
+   arrow
+   options_management
+   stateless
+   c_backend_common
+   typing
+   ocaml_utils
+   backends
+   lustrec_mpfr
+   normalization
+   machine_types
+   splitting
+   compiler_common
+   parse parser_lustre lexer_lustre lexerLustreSpec
+   automata
+   clock_calculus
+ )
+ (wrapped false)
+ (libraries ocamlgraph zarith unix str))
+
+(library
+ (name plugin_register)
+ (package lustrec)
+ (wrapped false)
+ (modules pluginList pluginType)
+ (libraries lustrec_interface))
+
+(generate_sites_module
+ (module sites)
+ (plugins (lustrec plugins) (lustrec verifiers)))
+
+(library
+ (name sites)
+ (package lustrec)
+ (modules sites)
+ (libraries dune-site dune-site.plugins))
+
+(library
+ (name lustrec_lib)
+ (package lustrec)
+ (modules
+   lusic
+   c_backend_header c_backend_spec c_backend_makefile
+   c_backend_lusic c_backend_mauve c_backend_src
+   ada_backend ada_printer ada_backend_common ada_backend_ads ada_backend_adb
+   ada_backend_wrapper
+   horn_backend horn_backend_common horn_backend_printers
+   Horn_backend_collecting_sem horn_backend_traces
+   EMF_backend EMF_common EMF_library_calls
+   misc_lustre_function misc_printer
+   machine_code
+   causality
+   scheduling
+   liveness
+   compiler_stages
+   modules
+   sortProg
+   inliner
+   access
+   algebraicLoop
+   optimize_prog
+   optimize_machine
+   spec
+   c_backend c_backend_main
+   plugins
+ )
+ (wrapped false)
+ (libraries sites lustrec_interface plugin_register))
+
+(executable
+ (name main_lustre_compiler)
+ (public_name lustrec)
+ (modules main_lustre_compiler)
+ (package lustrec)
+ (libraries lustrec_lib lustrec.scopes))
+
+(executable
+ (name main_lustre_testgen)
+ (public_name lustret)
+ (modules main_lustre_testgen mutation mmap pathConditions)
+ (libraries lustrec_lib))
+
+(library
+ (name verifier_register)
+ (package lustrec)
+ (wrapped false)
+ (modules verifierList verifierType)
+ (libraries lustrec_interface))
+
+(executable
+ (name main_lustre_verifier)
+ (public_name lustrev)
+ (modules main_lustre_verifier verifiers)
+ (libraries lustrec_lib verifier_register lustrec.scopes))
diff --git a/src/features/.merlin b/src/features/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/features/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/features/machine_types/.merlin b/src/features/machine_types/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/features/machine_types/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/machine_code.ml b/src/machine_code.ml
index c964e96db6703fe6e8490f99922d6fd6c8b79680..e80233bf4ca6c3acd46bf5ff788e8b75b5264b50 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -227,12 +227,12 @@ let translate_eq env ctx eq =
   match eq.eq_lhs, eq.eq_rhs.expr_desc with
   | [x], Expr_arrow (e1, e2)                     ->
      let var_x = env.get_var x in
-     let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
+     let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
      let c1 = translate_expr e1 in
      let c2 = translate_expr e2 in
      { ctx with
        si = mkinstr (MReset o) :: ctx.si;
-       j = Utils.IMap.add o (Arrow.arrow_top_decl, []) ctx.j;
+       j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
        s = (control_on_clock
               eq.eq_rhs.expr_clock
               (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
diff --git a/src/ocaml_utils.ml.in b/src/ocaml_utils.ml.in
deleted file mode 100644
index 09a45753fdcb418fe2b64c398f5cedcb48333421..0000000000000000000000000000000000000000
--- a/src/ocaml_utils.ml.in
+++ /dev/null
@@ -1 +0,0 @@
-let uppercase = @UPPERCASEFUN@
diff --git a/src/options_management.ml b/src/options_management.ml
index acc58285b880279bf1180c1bd390a00fe6e455e0..cfc14857b490cecc5ed3bf0e22c5e64c62d373d2 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -52,7 +52,8 @@ let search_lib_path (local, full_file_name) =
   in
   match name with
   | None ->
-     Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;
+    Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name
+      (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;
      raise Not_found
   | Some s -> s
 
diff --git a/src/parsers/.merlin b/src/parsers/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/parsers/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/parsers/dune b/src/parsers/dune
new file mode 100644
index 0000000000000000000000000000000000000000..16d76189eb412faefdec057eb0932dbc1060e919
--- /dev/null
+++ b/src/parsers/dune
@@ -0,0 +1,12 @@
+; (include_subdirs no)
+
+; (library
+;  (name parse)
+;  (package lustrec)
+;  (wrapped false)
+;  (libraries lustre_types corelang automata))
+
+(menhir
+ (modules parser_lustre))
+
+(ocamllex lexerLustreSpec lexer_lustre)
diff --git a/src/parsers/parse.ml b/src/parsers/parse.ml
index 69909045ad85fba970fa2a295fe3bf0e733ccf9b..c33319cf38ea56f3eac866734edb2687aaee7bc4 100644
--- a/src/parsers/parse.ml
+++ b/src/parsers/parse.ml
@@ -9,8 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 open Format
-open Lustre_types
-open Corelang
 
 type error =
   | Undefined_token of string
diff --git a/src/pluginList.ml.in b/src/pluginList.ml.in
deleted file mode 100644
index 6efbd219c678da918829f5de7a63a5046874ea01..0000000000000000000000000000000000000000
--- a/src/pluginList.ml.in
+++ /dev/null
@@ -1,5 +0,0 @@
-let plugins =
-  [
-    (module Scopes.Plugin : PluginType.S);
-    @SALSA@
-  ]
diff --git a/src/plugins/.merlin b/src/plugins/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/plugins/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/mpfr/.merlin b/src/plugins/mpfr/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/plugins/mpfr/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/pluginList.ml b/src/plugins/pluginList.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ad10f5471c5daa59048430b1e583ea62a1be94c3
--- /dev/null
+++ b/src/plugins/pluginList.ml
@@ -0,0 +1,3 @@
+let registered : (module PluginType.S) list ref = ref []
+
+let plugins () = !registered
diff --git a/src/pluginType.ml b/src/plugins/pluginType.ml
similarity index 100%
rename from src/pluginType.ml
rename to src/plugins/pluginType.ml
diff --git a/src/plugins.ml b/src/plugins/plugins.ml
similarity index 85%
rename from src/plugins.ml
rename to src/plugins/plugins.ml
index 219d4e56925667038cbe96d49c0a95e6eb8c469b..e7e9689d34c66f7596cf7351f85d15d7fba0e325 100644
--- a/src/plugins.ml
+++ b/src/plugins/plugins.ml
@@ -2,6 +2,7 @@ open Lustre_types
 
 open PluginList
 
+let () = Sites.Plugins.Plugins.load_all ()
 
 let options () = 
   List.flatten (
@@ -9,37 +10,37 @@ let options () =
       List.map (fun m ->
 	let module M = (val m : PluginType.S) in
 	(M.name, M.activate, M.usage, M.options)
-      ) plugins
+      ) (plugins ())
     ))
 
 let init () =
   List.iter (fun m ->
       let module M = (val m : PluginType.S) in
       M.init ()
-    ) plugins
+    ) (plugins ())
   
 let check_force_stateful () =
   List.exists (fun m ->
 	let module M = (val m : PluginType.S) in
 	M.check_force_stateful ()
-  ) plugins
+  ) (plugins ())
 
 let refine_machine_code prog machine_code =
   List.fold_left (fun accu m ->
     let module M = (val m : PluginType.S) in
     M.refine_machine_code prog accu
-  ) machine_code plugins
+  ) machine_code (plugins ())
 
 
 let c_backend_main_loop_body_prefix basename mname fmt () = 
   List.iter (fun (m: (module PluginType.S)) -> 
     let module M = (val m : PluginType.S) in
-    M.c_backend_main_loop_body_prefix basename mname fmt ()) plugins
+    M.c_backend_main_loop_body_prefix basename mname fmt ()) (plugins ())
 
 let c_backend_main_loop_body_suffix fmt () = 
   List.iter (fun (m: (module PluginType.S)) -> 
     let module M = (val m : PluginType.S) in
-    M.c_backend_main_loop_body_suffix fmt ()) plugins
+    M.c_backend_main_loop_body_suffix fmt ()) (plugins ())
 
 (* Specific treatment of annotations when inlining, specific of declared plugins *)
 
diff --git a/src/plugins/salsa/.merlin b/src/plugins/salsa/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/plugins/salsa/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/salsa/dune b/src/plugins/salsa/dune
new file mode 100644
index 0000000000000000000000000000000000000000..70fbbfff5fd9420aa6a5ac713947eeda4ee064bf
--- /dev/null
+++ b/src/plugins/salsa/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name salsa_plugin)
+ (public_name lustrec.salsa_plugin)
+ (libraries lustrec_interface plugin_register salsa)
+ (optional))
+
+(plugin
+ (name salsa_plugin)
+ (libraries lustrec.salsa_plugin)
+ (site (lustrec plugins))
+ (optional))
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
index 1bbf6ca23a66a5e670674e20c32f883f32fbd747..a16909ab0fb9e8418cd77c03996ceb19a98b1a2d 100644
--- a/src/plugins/salsa/salsa_plugin.ml
+++ b/src/plugins/salsa/salsa_plugin.ml
@@ -54,3 +54,7 @@ module Plugin =
   
   
  end: PluginType.S)
+
+let () =
+  PluginList.registered := (module Plugin : PluginType.S) ::
+                           !PluginList.registered
diff --git a/src/plugins/scopes/.merlin b/src/plugins/scopes/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/plugins/scopes/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/plugins/scopes/dune b/src/plugins/scopes/dune
new file mode 100644
index 0000000000000000000000000000000000000000..b110b1f31a73359140483e6ce79414622909e49b
--- /dev/null
+++ b/src/plugins/scopes/dune
@@ -0,0 +1,11 @@
+(include_subdirs no)
+
+(library
+ (name scopes)
+ (public_name lustrec.scopes)
+ (libraries lustrec_interface plugin_register))
+
+(plugin
+ (name scopes_plugin)
+ (libraries lustrec.scopes)
+ (site (lustrec plugins)))
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index ae7e473d5d89153747641d5ee184fe66e499e925..daa75f4c5157fd8236a79d6d159c67b02aa02e02 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -422,7 +422,10 @@ module Plugin : (
 
 
 end
-    
+
+let () =
+  PluginList.registered := (module Plugin : PluginType.S) ::
+                           !PluginList.registered
 (* Local Variables: *)
 (* compile-command:"make -C ../.." *)
 (* End: *)
diff --git a/src/tools/.merlin b/src/tools/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/seal/dune b/src/tools/seal/dune
new file mode 100644
index 0000000000000000000000000000000000000000..2f77ac7d07d4c64d60d252115a9567b138a12b28
--- /dev/null
+++ b/src/tools/seal/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name seal_verifier)
+ (public_name lustrec.seal_verifier)
+ (libraries verifier_register lustrec_lib zustre_verifier)
+ (optional))
+
+(plugin
+ (name seal_verifier)
+ (libraries lustrec.seal_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/seal/seal_verifier.ml b/src/tools/seal/seal_verifier.ml
index 4802d2179f16a3ccec37bec0b1aab24342dd9b89..fed38147d448b158f2ce9726766af9a48b98dacf 100644
--- a/src/tools/seal/seal_verifier.ml
+++ b/src/tools/seal/seal_verifier.ml
@@ -157,3 +157,6 @@ module Verifier =
             
   end: VerifierType.S)
     
+let () =
+  VerifierList.registered := (module Verifier : VerifierType.S) ::
+                             !VerifierList.registered
diff --git a/src/tools/stateflow/.merlin b/src/tools/stateflow/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/stateflow/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/common/.merlin b/src/tools/stateflow/common/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/stateflow/common/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/json-parser/.merlin b/src/tools/stateflow/json-parser/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/stateflow/json-parser/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/models/.merlin b/src/tools/stateflow/models/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/stateflow/models/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/semantics/.merlin b/src/tools/stateflow/semantics/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/tools/stateflow/semantics/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/tools/stateflow/semantics/cPS_evaluator.ml b/src/tools/stateflow/semantics/cPS_evaluator.ml
index 896252ca48fbbb94fc224943cc1ec1898a3d751d..c15d501d9ab2e7932fec1dc141ea642873da7654 100644
--- a/src/tools/stateflow/semantics/cPS_evaluator.ml
+++ b/src/tools/stateflow/semantics/cPS_evaluator.ml
@@ -7,7 +7,7 @@
      - Evaluator module
  *)
 
-  let _main_ _ = 
+  let _main_ _ = function
     | Eval ->
      let module Model = (val model) in
      let module T = CPS_transformer.Evaluator in
diff --git a/src/tools/tiny/dune b/src/tools/tiny/dune
new file mode 100644
index 0000000000000000000000000000000000000000..2242ea1a390cf1e676c308e61632defcadedb35e
--- /dev/null
+++ b/src/tools/tiny/dune
@@ -0,0 +1,13 @@
+(include_subdirs no)
+
+(library
+ (name tiny_verifier)
+ (public_name lustrec.tiny_verifier)
+ (libraries verifier_register tiny)
+ (optional))
+
+(plugin
+ (name tiny_verifier)
+ (libraries lustrec.tiny_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/tiny/tiny_verifier.ml b/src/tools/tiny/tiny_verifier.ml
index 0f903a21dfc33a61cc0c6c34ea1bce8932e5de03..071e1430295b1acd7401fac0dbea2ab449dfbf99 100644
--- a/src/tools/tiny/tiny_verifier.ml
+++ b/src/tools/tiny/tiny_verifier.ml
@@ -135,4 +135,7 @@ module Verifier =
             
             
   end: VerifierType.S)
-    
+
+let () =
+  VerifierList.registered := (module Verifier : VerifierType.S) ::
+                             !VerifierList.registered
diff --git a/src/tools/zustre/dune b/src/tools/zustre/dune
new file mode 100644
index 0000000000000000000000000000000000000000..0b5140f99df3b3aadbe815b0be83723674eb7e7c
--- /dev/null
+++ b/src/tools/zustre/dune
@@ -0,0 +1,15 @@
+(include_subdirs no)
+
+(library
+ (name zustre_verifier)
+ (public_name lustrec.zustre_verifier)
+ (wrapped false)
+ (modules :standard \ zustre_test)
+ (libraries verifier_register lustrec_lib z3 yojson)
+ (optional))
+
+(plugin
+ (name zustre_verifier)
+ (libraries lustrec.zustre_verifier)
+ (site (lustrec verifiers))
+ (optional))
diff --git a/src/tools/zustre/zustre_verifier.ml b/src/tools/zustre/zustre_verifier.ml
index 12281ff459d81a359d7baa4b7e69f10a8ff2bd15..337654c956505e4897f6e83364fb29874c82b45b 100644
--- a/src/tools/zustre/zustre_verifier.ml
+++ b/src/tools/zustre/zustre_verifier.ml
@@ -264,7 +264,12 @@ module Verifier =
 	
 
 	    end: VerifierType.S)
-    
+
+
+let () =
+  VerifierList.registered := (module Verifier : VerifierType.S) ::
+                             !VerifierList.registered
+
 (* Local Variables: *)
 (* compile-command:"make -C ../.. lustrev" *)
 (* End: *)
diff --git a/src/utils/.merlin b/src/utils/.merlin
deleted file mode 100644
index 2fb3f0bc1e7fdfef783204d7f14fd522a606bd77..0000000000000000000000000000000000000000
--- a/src/utils/.merlin
+++ /dev/null
@@ -1 +0,0 @@
-REC
\ No newline at end of file
diff --git a/src/dimension.ml b/src/utils/dimension.ml
similarity index 100%
rename from src/dimension.ml
rename to src/utils/dimension.ml
diff --git a/src/utils/dune b/src/utils/dune
new file mode 100644
index 0000000000000000000000000000000000000000..064da44eb7f1c433b838d5ddd5070f3920df0ce4
--- /dev/null
+++ b/src/utils/dune
@@ -0,0 +1,18 @@
+; (include_subdirs no)
+
+(rule
+ (target ocaml_utils.ml)
+ (deps ocaml_utils.ml.lt403)
+ (action (copy %{deps} %{target}))
+ (enabled_if (< %{ocaml_version} 4.0.3)))
+(rule
+ (target ocaml_utils.ml)
+ (deps ocaml_utils.ml.ge403)
+ (action (copy %{deps} %{target}))
+ (enabled_if (>= %{ocaml_version} 4.0.3)))
+
+; (library
+;  (name utils)
+;  (package lustrec)
+;  (wrapped false)
+;  (libraries ocamlgraph unix))
diff --git a/src/location.ml b/src/utils/location.ml
similarity index 100%
rename from src/location.ml
rename to src/utils/location.ml
diff --git a/src/utils/ocaml_utils.ml.ge403 b/src/utils/ocaml_utils.ml.ge403
new file mode 100644
index 0000000000000000000000000000000000000000..90fadc64d88d80b99ab69885dc486cdb0280dc9d
--- /dev/null
+++ b/src/utils/ocaml_utils.ml.ge403
@@ -0,0 +1 @@
+let uppercase = String.uppercase_ascii
diff --git a/src/utils/ocaml_utils.ml.lt403 b/src/utils/ocaml_utils.ml.lt403
new file mode 100644
index 0000000000000000000000000000000000000000..41db848f22c43237f4e8f7454b13350f5e530326
--- /dev/null
+++ b/src/utils/ocaml_utils.ml.lt403
@@ -0,0 +1 @@
+let uppercase = String.uppercase
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 89d1be33652004832e86eebf09c1bb0ce9955223..f1c661dcde4f30e770de2ff32758331fc482c984 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -428,7 +428,6 @@ let get_date () =
   Format.flush_str_formatter ()
 
 
-                           
                            (* Local Variables: *)
                            (* compile-command:"make -C .." *)
                            (* End: *)
diff --git a/src/verifierList.ml b/src/verifierList.ml
new file mode 100644
index 0000000000000000000000000000000000000000..254cda864a0d835b5f75d0b0e50e0519d124a91d
--- /dev/null
+++ b/src/verifierList.ml
@@ -0,0 +1,8 @@
+let registered : (module VerifierType.S) list ref = ref []
+
+let verifiers () = !registered
+  (* [
+   *   @LUSTREV_SEAL@
+   *   @LUSTREV_ZUSTRE@
+   *   @LUSTREV_TINY@
+   * ] *)
diff --git a/src/verifierList.ml.in b/src/verifierList.ml.in
deleted file mode 100644
index 322949a260fe541c5c2c7af0c5e05e98dabe74df..0000000000000000000000000000000000000000
--- a/src/verifierList.ml.in
+++ /dev/null
@@ -1,6 +0,0 @@
-let verifiers =
-  [
-    @LUSTREV_SEAL@
-    @LUSTREV_ZUSTRE@
-    @LUSTREV_TINY@
-  ]
diff --git a/src/verifiers.ml b/src/verifiers.ml
index e36bfd9e9776ff8610b8d65b19b3089cbdfa986c..baac4bc0a9de1e89c543cfe4a9a58207ce3e6a47 100644
--- a/src/verifiers.ml
+++ b/src/verifiers.ml
@@ -2,6 +2,8 @@ open Lustre_types
 
 open VerifierList
 
+let () = Sites.Plugins.Verifiers.load_all ()
+
 let active = ref None
            
 let options () = 
@@ -10,7 +12,7 @@ let options () =
       List.map (fun m ->
 	let module M = (val m : VerifierType.S) in
 	(M.name, M.activate, M.options)
-      ) verifiers
+      ) (verifiers ())
     ))
   
 let verifier_list verifiers =
@@ -31,10 +33,10 @@ let get_active () =
                m::found
              else
                found
-           ) [] verifiers
+           ) [] (verifiers ())
        in
        match found with
-       | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))
+       | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list (verifiers ())))
        | [m] -> active := Some m; m
        | _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))
      end
diff --git a/src/version.ml.in b/src/version.ml
similarity index 99%
rename from src/version.ml.in
rename to src/version.ml
index 19e9233c49a8dd9129bcd7dde86c4ae2128b56d4..30f5044e61a39a20b1ee975effe2a234e0a78162 100644
--- a/src/version.ml.in
+++ b/src/version.ml
@@ -1,4 +1,3 @@
-
 let number = "@PACKAGE_VERSION@-@GITBRANCH@"
 
 let codename ="@VERSION_CODENAME@"