diff --git a/.travis.yml b/.travis.yml
index 2004ee09b..070206301 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,9 +43,8 @@ matrix:
     - eval $(opam env)
     - opam install -j $JOBS -y $PREDEPS
     - opam install -j $JOBS -y $DEPS
-    - make
-    - make -C tests run
-    - make byte
+    - dune build
+    - make tests
 
   - env: TEST="linux build $OCAML_MAX"
     os: linux
@@ -66,9 +65,8 @@ matrix:
     - eval $(opam env)
     - opam install -j $JOBS -y $PREDEPS
     - opam install -j $JOBS -y $DEPS
-    - make
-    - make -C tests run
-    - make byte
+    - dune build
+    - make tests
 
   - env: TEST="osx build $OCAML_MIN"
     os: osx
@@ -85,9 +83,8 @@ matrix:
     - eval $(opam env)
     - opam install -j $JOBS -y $PREDEPS
     - opam install -j $JOBS -y $DEPS
-    - make
-    - make -C tests run
-    - make byte
+    - dune build
+    - make tests
 
   - env: TEST="osx build $OCAML_MAX"
     os: osx
@@ -104,9 +101,8 @@ matrix:
     - eval $(opam env)
     - opam install -j $JOBS -y $PREDEPS
     - opam install -j $JOBS -y $DEPS
-    - make
-    - make -C tests run
-    - make byte
+    - dune build
+    - make tests
 
   - env: TEST="opam package installation"
     os: linux
diff --git a/Makefile b/Makefile
index c0adc8699..2c27d23f0 100644
--- a/Makefile
+++ b/Makefile
@@ -1,134 +1,46 @@
-# Commands:
-#  make                        -- to compile elpi
-#  make install                -- to install elpi using findlib
-#  make install-bin BIN=path   -- to install the elpi REPL in $BIN
-#  make uninstall              -- to remove elpi using findlib
-#  make uninstall-bin BIN=path -- to remove the elpi REPL in $BIN
-#  ... BYTE=yes                -- to compile/install/remove byte code
-#
-#  make git/V -- to compile elpi.git.V out of git's commit/branch/tag V
-#                such binary is then picked up automatically by the bench
-#                system as an elpi like runner
-#  make runners -- foreach git tag runner-V, do something like make git/V 
 
-BASE=$(shell pwd)
-include Makefile.common
-
-all: check-ocaml-ver elpi$(EXE) builtin.elpi
-
-byte:
-	$(H)$(MAKE) BYTE=1 all
-
-trace_ppx: trace_ppx.ml
-	$(H)$(call pp,OCAMLOPT,-o,$@)
-	$(H)ocamlfind ocamlopt \
-		-package ppx_tools_versioned \
-		-package ppx_tools_versioned.metaquot_402 \
-		-package ocaml-migrate-parsetree.driver-main \
-		-open Ast_402 \
-		-c $< 
-	$(H)ocamlfind ocamlopt \
-		-package ppx_tools_versioned \
-		-package ppx_tools_versioned.metaquot_402 \
-		-package ocaml-migrate-parsetree \
-		-predicates custom_ppx,ppx_driver \
-		-linkpkg -linkall \
-		trace_ppx.cmx \
-		`ocamlfind query -predicates native \
-	       		ocaml-migrate-parsetree.driver-main -a-format` \
-		-o $@
-	$(H)cp .merlin.in .merlin
-	$(H)echo "FLG -ppx '$(shell pwd)/trace_ppx --as-ppx'" >> .merlin
+help:
+	@echo 'Known targets:'
+	@echo
+	@echo '  tests            runs the entire test suite'
+	@echo '  tests ONLY=rex   runs only tests matching rex'
+	@echo
+	@echo '  git/treeish      checkout treeish and build elpi.git.treeish'
+	@echo
+
+INSTALL=_build/install/default
+BUILD=_build/default
+SHELL:=/bin/bash
+TIMEOUT=60.0
+RUNNERS=\
+  $(shell pwd)/$(INSTALL)/bin/elpi \
+  $(addprefix $(shell pwd)/,$(wildcard elpi.git.*)) \
+  $(shell if type tjsim >/dev/null 2>&1; then type -P tjsim; else echo; fi)
+TIME=$(shell if type -P gtime >/dev/null 2>&1; then type -P gtime; else echo /usr/bin/time; fi)
+STACK=32768
+
+tests:
+	dune build $(INSTALL)/bin/elpi
+	dune build $(BUILD)/tests/test.exe
+	ulimit -s $(STACK); \
+		$(BUILD)/tests/test.exe \
+		--seed $$RANDOM \
+		--timeout $(TIMEOUT) \
+		--time=$(TIME) \
+		--sources=$$PWD/tests/sources/ \
+		--plot=$$PWD/tests/plot \
+		$(addprefix --name-match ,$(ONLY)) \
+		$(addprefix --runner , $(RUNNERS))
 
 git/%:
-	$(H)rm -rf "$$PWD/elpi-$*"
-	$(H)mkdir "elpi-$*"
-	$(H)git clone -l . "elpi-$*"
-	$(H)cd "elpi-$*" && git checkout "$*" && make
-	$(H)cp "elpi-$*/elpi" "elpi.git.$*"
-	$(H)rm -rf "$$PWD/elpi-$*"
-
-runners:
-	$(H)true $(foreach t,$(shell git branch --list 'runner*' | cut -c 3-),\
-		&& $(MAKE) git/$(t) && \
-		mv elpi.git.$(t) elpi.git.$(t:runner-%=%))
-
-clean:
-	$(H)rm -f $(addprefix src/, $(TRASH))
-	$(H)rm -f $(TRASH)
-	$(H)rm -f trace_ppx.cmx elpi_config.ml
-	$(H)rm -f elpi.git.* trace_ppx elpi elpi.byte
-	$(H)rm -f src/.depends src/.depends.parser 
-	$(H)rm -f src/.depends.byte src/.depends.parser.byte
-	$(H)rm -rf findlib/
-
-dist:
-	$(H)git archive --format=tar --prefix=elpi-$(V)/ HEAD . \
-		| gzip > ../elpi-$(V).tgz
-
-# compilation of elpi
-
-OC_OPTIONS = -linkpkg $(OCAMLOPTIONS) $(FLAGS)
-
-ELPI_LIBS = \
-  elpi_quoted_syntax.elpi  elpi-checker.elpi  \
-  utils/elpi2html.elpi
-
-ELPI_DIST = \
-  $(addprefix src/,elpi_API.cmi elpi_API.mli elpi_builtin.cmi elpi_builtin.mli elpi.cmi)
-
-ELPI_DIST_OPT = \
-  $(addprefix src/,elpi.cma elpi.cmxa elpi.a elpi_builtin.cmti elpi_API.cmti elpi_API.cmx elpi_API.cmo elpi_builtin.cmo elpi_builtin.cmx)
-
-elpi$(EXE): elpi_REPL.ml elpi_config.$(CMX) findlib/elpi/META
-	$(H)$(call pp,$(OCNAME),-package elpi elpi_config.$(CMX) -o $@,$<)
-	$(H)$(OC) $(OC_OPTIONS) -package elpi elpi_config.$(CMX) -o $@ $<
-
-elpi_config.$(CMX): elpi_config.ml elpi_config.cmi
-	$(H)$(call pp,$(OCNAME),-c, $<)
-	$(H)$(OC) $(OC_OPTIONS) -c $<
-
-elpi_config.cmi: elpi_config.mli
-	$(H)$(call pp,$(OCNAME),-c, $<)
-	$(H)$(OC) $(OC_OPTIONS) -c $<
-
-builtin.elpi: elpi$(EXE)
-	$(H)echo '%% File generated by elpi -document-builtins, do not edit' > $@
-	$(H)./elpi -document-builtins >> $@
-
-elpi_config.ml:
-	$(H)echo 'let install_dir = "$(shell ocamlfind printconf destdir)/elpi"' > $@
-
-src/%: | trace_ppx
-	$(H)$(MAKE) --no-print-directory -C src/ $*
-
-src/elpi.$(CMXA): $(wildcard src/*.ml) $(wildcard src/*.mli)
-findlib/elpi/META: src/elpi.$(CMXA) Makefile
-	$(H)rm -rf findlib/; mkdir findlib
-	$(H)$(MAKE) --no-print-directory -C src/ elpi.cmi # needed by ELPI_DIST
-	$(H)ocamlfind install -destdir $(BASE)/findlib -patch-archives \
-		elpi META $(ELPI_DIST) $(ELPI_LIBS) \
-		-optional $(ELPI_DIST_OPT)
-
-install:
-	$(H)ocamlfind install -patch-archives \
-		elpi META $(ELPI_DIST) $(ELPI_LIBS) \
-		-optional $(ELPI_DIST_OPT) elpi elpi.byte
-install-bin:
-	$(H)cp elpi$(EXE) $(BIN)
-
-uninstall:
-	$(H)ocamlfind remove elpi
-uninstall-bin:
-	$(H)rm -f $(BIN)/elpi$(EXE)
-
-
-# required OCaml package
-check-ocaml-ver:
-	$(H)ocamlfind query camlp5 > /dev/null
-	$(H)ocamlfind query ppx_tools_versioned > /dev/null
-	$(H)ocamlfind query ppx_deriving > /dev/null
-	$(H)ocamlfind query ocaml-migrate-parsetree.driver-main > /dev/null
-	$(H)ocamlfind query re.str > /dev/null
-
-.NOTPARALLEL:
+	rm -rf "$$PWD/elpi-$*"
+	mkdir "elpi-$*"
+	git clone -l . "elpi-$*"
+	cd "elpi-$*" && git checkout "$*"
+	cd "elpi-$*" && \
+	  if [ -f dune ]; then dune build --root . @install; else make; fi
+	cp "elpi-$*/elpi" "elpi.git.$*" || \
+		cp "elpi-$*/$(INSTALL)/bin/elpi" "elpi.git.$*"
+	rm -rf "$$PWD/elpi-$*"
+
+.PHONY: tests all install uninstall help
diff --git a/Makefile.common b/Makefile.common
deleted file mode 100644
index 7e3b242ab..000000000
--- a/Makefile.common
+++ /dev/null
@@ -1,34 +0,0 @@
-# We expect the user to define BASE to the root of the repo
-
-V=$(shell git describe --tags)
-PP=camlp5o -I . -I +camlp5
-PARSE=pa_extend.cmo pa_lexer.cmo
-FLAGS=-I $(shell camlp5 -where) -w +a
-OCAMLOPTIONS= -g -bin-annot
-OD=ocamlfind ocamldep
-
-ifeq "$(BYTE)" ""
-CMX=cmx
-CMXA=cmxa
-EXE=
-OC=ocamlfind ocamlopt
-DEPS=.depends .depends.parser
-OCNAME=OCAMLOPT
-OOPAQUE=
-else
-CMX=cmo
-CMXA=cma
-EXE=.byte
-OC=ocamlfind ocamlc
-DEPS=.depends.byte .depends.parser.byte
-OCNAME=OCAMLC
-OOPAQUE=
-endif
-
-ifeq "$(findstring install,$(MAKECMDGOALS))$(findstring uninstall,$(MAKECMDGOALS))" ""
-OCAMLPATH:=$(BASE)/findlib:$(OCAMLPATH)
-export OCAMLPATH
-endif
-H=@
-pp = printf '$(1) %-26s %s\n' "$(3)" "$(2)"
-TRASH=*.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a *.cmt *.cmti
diff --git a/README.md b/README.md
index 1185e0a3a..c57bb7505 100644
--- a/README.md
+++ b/README.md
@@ -30,8 +30,7 @@ you can type
 ```
 opam pin add elpi https://github.com/LPCIC/elpi.git
 ```
-You can also clone this repository and type `make`.  The build requirements
-are listed at the end of the [Makefile](Makefile)
+You can also clone this repository and type `dune build`.
 
 #### Syntax highlight in vim
 
@@ -126,7 +125,7 @@ by Miller and Nadathur is highly recommended and covers standard λProlog.
 
 The extensions to λProlog implemented in ELPI are described in the
 [ELPI](ELPI.md) file, built-in predicates are documented in
-[builtin](builtin.elpi).
+[builtin](src/builtin.elpi).
 
 There is a [short paper](https://hal.inria.fr/hal-01176856/) describing
 the implementation of the interpreter, in particular how it deals with
diff --git a/dune b/dune
new file mode 100644
index 000000000..6e308ec29
--- /dev/null
+++ b/dune
@@ -0,0 +1,7 @@
+(executable
+  (name elpi_REPL)
+  (public_name elpi)
+  (libraries elpi)
+  (modules elpi_REPL)
+)
+
diff --git a/dune-project b/dune-project
new file mode 100644
index 000000000..bb48ee3e8
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,2 @@
+(lang dune 1.6)
+(name "elpi")
diff --git a/elpi.install b/elpi.install
new file mode 100644
index 000000000..04e538026
--- /dev/null
+++ b/elpi.install
@@ -0,0 +1,97 @@
+lib: [
+  "_build/install/default/lib/elpi/META" {"META"}
+  "_build/install/default/lib/elpi/builtin.elpi"
+  "_build/install/default/lib/elpi/elpi-checker.elpi"
+  "_build/install/default/lib/elpi/elpi.a" {"elpi.a"}
+  "_build/install/default/lib/elpi/elpi.cma" {"elpi.cma"}
+  "_build/install/default/lib/elpi/elpi.cmi" {"elpi.cmi"}
+  "_build/install/default/lib/elpi/elpi.cmt" {"elpi.cmt"}
+  "_build/install/default/lib/elpi/elpi.cmx" {"elpi.cmx"}
+  "_build/install/default/lib/elpi/elpi.cmxa" {"elpi.cmxa"}
+  "_build/install/default/lib/elpi/elpi.cmxs" {"elpi.cmxs"}
+  "_build/install/default/lib/elpi/elpi.dune" {"elpi.dune"}
+  "_build/install/default/lib/elpi/elpi.ml" {"elpi.ml"}
+  "_build/install/default/lib/elpi/elpi2html.elpi"
+  "_build/install/default/lib/elpi/elpi_API.ml" {"elpi_API.ml"}
+  "_build/install/default/lib/elpi/elpi_API.mli" {"elpi_API.mli"}
+  "_build/install/default/lib/elpi/elpi__.cmi" {"elpi__.cmi"}
+  "_build/install/default/lib/elpi/elpi__.cmt" {"elpi__.cmt"}
+  "_build/install/default/lib/elpi/elpi__.cmx" {"elpi__.cmx"}
+  "_build/install/default/lib/elpi/elpi__.ml" {"elpi__.ml"}
+  "_build/install/default/lib/elpi/elpi__Elpi_API.cmi" {"elpi__Elpi_API.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_API.cmt" {"elpi__Elpi_API.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_API.cmti" {"elpi__Elpi_API.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_API.cmx" {"elpi__Elpi_API.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ast.cmi" {"elpi__Elpi_ast.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ast.cmt" {"elpi__Elpi_ast.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ast.cmti" {"elpi__Elpi_ast.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ast.cmx" {"elpi__Elpi_ast.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmi" {"elpi__Elpi_builtin.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmt" {"elpi__Elpi_builtin.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmti" {"elpi__Elpi_builtin.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmx" {"elpi__Elpi_builtin.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmi" {"elpi__Elpi_compiler.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmt" {"elpi__Elpi_compiler.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmti" {"elpi__Elpi_compiler.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmx" {"elpi__Elpi_compiler.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_data.cmi" {"elpi__Elpi_data.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_data.cmt" {"elpi__Elpi_data.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_data.cmx" {"elpi__Elpi_data.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_parser.cmi" {"elpi__Elpi_parser.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_parser.cmt" {"elpi__Elpi_parser.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_parser.cmti" {"elpi__Elpi_parser.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_parser.cmx" {"elpi__Elpi_parser.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmi" {"elpi__Elpi_ptmap.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmt" {"elpi__Elpi_ptmap.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmti" {"elpi__Elpi_ptmap.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmx" {"elpi__Elpi_ptmap.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmi" {"elpi__Elpi_runtime_trace_off.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmt" {"elpi__Elpi_runtime_trace_off.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmti" {"elpi__Elpi_runtime_trace_off.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmx" {"elpi__Elpi_runtime_trace_off.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmi" {"elpi__Elpi_runtime_trace_on.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmt" {"elpi__Elpi_runtime_trace_on.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmti" {"elpi__Elpi_runtime_trace_on.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmx" {"elpi__Elpi_runtime_trace_on.cmx"}
+  "_build/install/default/lib/elpi/elpi__Elpi_util.cmi" {"elpi__Elpi_util.cmi"}
+  "_build/install/default/lib/elpi/elpi__Elpi_util.cmt" {"elpi__Elpi_util.cmt"}
+  "_build/install/default/lib/elpi/elpi__Elpi_util.cmti" {"elpi__Elpi_util.cmti"}
+  "_build/install/default/lib/elpi/elpi__Elpi_util.cmx" {"elpi__Elpi_util.cmx"}
+  "_build/install/default/lib/elpi/elpi_ast.ml" {"elpi_ast.ml"}
+  "_build/install/default/lib/elpi/elpi_ast.mli" {"elpi_ast.mli"}
+  "_build/install/default/lib/elpi/elpi_builtin.ml" {"elpi_builtin.ml"}
+  "_build/install/default/lib/elpi/elpi_builtin.mli" {"elpi_builtin.mli"}
+  "_build/install/default/lib/elpi/elpi_compiler.ml" {"elpi_compiler.ml"}
+  "_build/install/default/lib/elpi/elpi_compiler.mli" {"elpi_compiler.mli"}
+  "_build/install/default/lib/elpi/elpi_data.ml" {"elpi_data.ml"}
+  "_build/install/default/lib/elpi/elpi_parser.ml" {"elpi_parser.ml"}
+  "_build/install/default/lib/elpi/elpi_parser.mli" {"elpi_parser.mli"}
+  "_build/install/default/lib/elpi/elpi_ptmap.ml" {"elpi_ptmap.ml"}
+  "_build/install/default/lib/elpi/elpi_ptmap.mli" {"elpi_ptmap.mli"}
+  "_build/install/default/lib/elpi/elpi_quoted_syntax.elpi"
+  "_build/install/default/lib/elpi/elpi_runtime_trace_off.ml" {"elpi_runtime_trace_off.ml"}
+  "_build/install/default/lib/elpi/elpi_runtime_trace_off.mli" {"elpi_runtime_trace_off.mli"}
+  "_build/install/default/lib/elpi/elpi_runtime_trace_on.ml" {"elpi_runtime_trace_on.ml"}
+  "_build/install/default/lib/elpi/elpi_runtime_trace_on.mli" {"elpi_runtime_trace_on.mli"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi.elpi_trace.dune" {"elpi_trace/elpi.elpi_trace.dune"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.a" {"elpi_trace/elpi_trace.a"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cma" {"elpi_trace/elpi_trace.cma"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmi" {"elpi_trace/elpi_trace.cmi"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmt" {"elpi_trace/elpi_trace.cmt"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmti" {"elpi_trace/elpi_trace.cmti"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmx" {"elpi_trace/elpi_trace.cmx"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxa" {"elpi_trace/elpi_trace.cmxa"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxs" {"elpi_trace/elpi_trace.cmxs"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.ml" {"elpi_trace/elpi_trace.ml"}
+  "_build/install/default/lib/elpi/elpi_trace/elpi_trace.mli" {"elpi_trace/elpi_trace.mli"}
+  "_build/install/default/lib/elpi/elpi_util.ml" {"elpi_util.ml"}
+  "_build/install/default/lib/elpi/elpi_util.mli" {"elpi_util.mli"}
+  "_build/install/default/lib/elpi/opam" {"opam"}
+]
+bin: [
+  "_build/install/default/bin/elpi" {"elpi"}
+]
+doc: [
+  "_build/install/default/doc/elpi/LICENSE"
+  "_build/install/default/doc/elpi/README.md"
+]
diff --git a/opam b/elpi.opam
similarity index 94%
rename from opam
rename to elpi.opam
index 9df00b422..e92b4d719 100644
--- a/opam
+++ b/elpi.opam
@@ -8,11 +8,13 @@ doc: "https://github.com/LPCIC/elpi"
 dev-repo: "git+https://github.com/LPCIC/elpi.git"
 bug-reports: "https://github.com/LPCIC/elpi/issues"
 
-build: [ [ make ] [ make "byte" ] ]
-run-test: [ make "-C" "tests" "run" ]
+build: [
+  [ "dune" "subst" {pinned} ]
+  [ "dune" "build" "-p" name "-j" jobs ]
+]
+run-test: [ make "tests" ]
 install: [ 
 	[ make "install" ]
-	[ make "install-bin" "BIN=%{bin}%" ]
 ]
 
 depends: [
@@ -22,6 +24,9 @@ depends: [
   "ppx_deriving"
   "ocaml-migrate-parsetree"
   "re" {>= "1.7.2"}
+  "dune" {build}
+  "ANSITerminal" {with-test}
+  "cmdliner" {with-test}
 ]
 synopsis: "ELPI - Embeddable λProlog Interpreter"
 description: """
diff --git a/elpi_REPL.ml b/elpi_REPL.ml
index 65c37d1bd..0860eb8b4 100644
--- a/elpi_REPL.ml
+++ b/elpi_REPL.ml
@@ -12,6 +12,7 @@ let _ =
   Gc.set tweaked_control
 ;;
 *)
+open Elpi
 
 module Str = Re.Str
 
@@ -55,7 +56,6 @@ let usage =
   "\nMain options:\n" ^ 
   "\t-test runs the query \"main\"\n" ^ 
   "\t-exec pred  runs the query \"pred ARGS\"\n" ^ 
-  "\t-where print system wide installation path then exit\n" ^ 
   "\t-D var  Define variable (conditional compilation)\n" ^ 
   "\t-document-builtins Print documentation for built-in predicates\n" ^
   "\t-no-tc don't typecheck the program\n" ^ 
@@ -88,8 +88,6 @@ let _ =
   let print_accumulated_files = ref false in
   let vars =
     ref Elpi_API.Compile.(default_flags.defined_variables) in
-  if List.mem "-where" (Array.to_list Sys.argv) then begin
-    Printf.printf "%s\n" Elpi_config.install_dir; exit 0 end;
   let rec aux = function
     | [] -> []
     | "-delay-problems-outside-pattern-fragment" :: rest -> delay_outside_fragment := true; aux rest
@@ -115,7 +113,10 @@ let _ =
     let v = try Sys.getenv "TJPATH" with Not_found -> "" in
     let tjpath = Str.split (Str.regexp ":") v in
     List.flatten (List.map (fun x -> ["-I";x]) tjpath) in
-  let installpath = [ "-I"; Elpi_config.install_dir ] in
+  let installpath = 
+    let v = try Sys.getenv "OCAMLPATH" with Not_found -> "" in
+    let ocamlpath = Str.split (Str.regexp ":") v in
+    List.flatten (List.map (fun x -> ["-I";x^"/elpi/"]) ocamlpath) in
   let execpath = ["-I"; Filename.dirname (Sys.executable_name)] in
   let opts = Array.to_list Sys.argv @ tjpath @ installpath @ execpath in
   let pheader, argv = Elpi_API.Setup.init ~builtins:Elpi_builtin.std_builtins opts ~basedir:cwd in
diff --git a/elpi_config.mli b/elpi_config.mli
deleted file mode 100644
index 9d93c1627..000000000
--- a/elpi_config.mli
+++ /dev/null
@@ -1,5 +0,0 @@
-(* elpi: embedded lambda prolog interpreter                                  *)
-(* license: GNU Lesser General Public License Version 2.1 or later           *)
-(* ------------------------------------------------------------------------- *)
-
-val install_dir : string
diff --git a/builtin.elpi b/src/builtin.elpi
similarity index 99%
rename from builtin.elpi
rename to src/builtin.elpi
index 4d699bf58..38fe8b469 100644
--- a/builtin.elpi
+++ b/src/builtin.elpi
@@ -1,5 +1,4 @@
-%% File generated by elpi -document-builtins, do not edit
-
+% File generated by elpi -document-builtins, do not edit
 
 %  == Core builtins =====================================
 
diff --git a/src/dune b/src/dune
new file mode 100644
index 000000000..d690eb0e7
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,48 @@
+(library
+  (name elpi)
+  (public_name elpi)
+  (preprocess (per_module
+    ((pps ppx_deriving.std trace_ppx --trace_ppx-on) elpi_runtime_trace_on)
+    ((pps ppx_deriving.std trace_ppx --trace_ppx-off) elpi_runtime_trace_off)
+    ((action (system "camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file}")) elpi_parser)
+    ((pps ppx_deriving.std) elpi_util elpi_ast elpi_data elpi_compiler)))
+  (libraries re.str camlp5.gramlib unix)
+  (flags -linkall)
+  (modules elpi elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_builtin elpi_API elpi_runtime_trace_on elpi_runtime_trace_off)
+)
+
+(rule
+  (targets elpi_runtime_trace_on.ml)
+  (deps elpi_runtime.ml)
+  (action (copy# %{deps} %{targets}))
+)
+(rule
+  (targets elpi_runtime_trace_on.mli)
+  (deps elpi_runtime.mli)
+  (action (copy# %{deps} %{targets}))
+)
+
+(rule
+  (targets elpi_runtime_trace_off.ml)
+  (deps elpi_runtime.ml)
+  (action (copy# %{deps} %{targets}))
+)
+(rule
+  (targets elpi_runtime_trace_off.mli)
+  (deps elpi_runtime.mli)
+  (action (copy# %{deps} %{targets}))
+)
+
+(install
+  (section lib)
+  (files builtin.elpi elpi-checker.elpi elpi_quoted_syntax.elpi elpi2html.elpi)
+)
+
+(rule
+  (targets builtin.elpi)
+  (mode promote)
+  (action (with-stdout-to %{targets}
+    (progn
+      (echo "% File generated by elpi -document-builtins, do not edit")
+      (run elpi -document-builtins))))
+)
diff --git a/elpi-checker.elpi b/src/elpi-checker.elpi
similarity index 100%
rename from elpi-checker.elpi
rename to src/elpi-checker.elpi
diff --git a/src/elpi.ml b/src/elpi.ml
new file mode 100644
index 000000000..93e7659e3
--- /dev/null
+++ b/src/elpi.ml
@@ -0,0 +1,2 @@
+module Elpi_API = Elpi_API
+module Elpi_builtin = Elpi_builtin
diff --git a/src/elpi.mli b/src/elpi.mli
deleted file mode 100644
index 0739863ab..000000000
--- a/src/elpi.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-(* elpi: embedded lambda prolog interpreter                                  *)
-(* license: GNU Lesser General Public License Version 2.1 or later           *)
-(* ------------------------------------------------------------------------- *)
-
diff --git a/utils/elpi2html.elpi b/src/elpi2html.elpi
similarity index 100%
rename from utils/elpi2html.elpi
rename to src/elpi2html.elpi
diff --git a/src/elpi_API.ml b/src/elpi_API.ml
index cf4cd6dc2..72e5a9c83 100644
--- a/src/elpi_API.ml
+++ b/src/elpi_API.ml
@@ -2,13 +2,13 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-module type Runtime = module type of Elpi_runtime_trace_off.Elpi_runtime
+module type Runtime = module type of Elpi_runtime_trace_off
 
-let r = ref (module Elpi_runtime_trace_off.Elpi_runtime : Runtime)
+let r = ref (module Elpi_runtime_trace_off : Runtime)
 
 let set_runtime = function
-  | true  -> r := (module Elpi_runtime_trace_on.Elpi_runtime  : Runtime)
-  | false -> r := (module Elpi_runtime_trace_off.Elpi_runtime : Runtime)
+  | true  -> r := (module Elpi_runtime_trace_on  : Runtime)
+  | false -> r := (module Elpi_runtime_trace_off : Runtime)
 
 let set_trace argv =
   let args = Elpi_trace.parse_argv argv in
diff --git a/src/elpi_compiler.ml b/src/elpi_compiler.ml
index 60a3c7824..06a267f6b 100644
--- a/src/elpi_compiler.ml
+++ b/src/elpi_compiler.ml
@@ -4,7 +4,7 @@
 
 open Elpi_util
 open Elpi_data
-open Elpi_runtime_trace_off.Elpi_runtime
+open Elpi_runtime_trace_off
 open Pp
 
 module C = Constants
diff --git a/elpi_quoted_syntax.elpi b/src/elpi_quoted_syntax.elpi
similarity index 100%
rename from elpi_quoted_syntax.elpi
rename to src/elpi_quoted_syntax.elpi
diff --git a/tests/Makefile b/tests/Makefile
deleted file mode 100644
index 52d3422fc..000000000
--- a/tests/Makefile
+++ /dev/null
@@ -1,43 +0,0 @@
-SHELL:=/bin/bash
-TIMEOUT=60.0
-RUNNERS=$(shell type -P ../elpi $(wildcard ../elpi.*)) $(shell if type tjsim >/dev/null 2>&1; then type -P tjsim; else echo; fi)
-TIME=$(shell if type -P gtime >/dev/null 2>&1; then type -P gtime; else echo /usr/bin/time; fi)
-BUILD=_build/default/
-STACK=32768
-
-help:
-	@echo 'Known targets:'
-	@echo
-	@echo '  build          build the test utility'
-	@echo '  man            manpage of the test utility'
-	@echo
-	@echo '  run            runs the entire test suite'
-	@echo '  run ONLY=rex   runs only tests matching rex'
-	@echo
-	@echo '  clean          purges _build _log and plots'
-	@echo
-	@echo 'Known runners:'
-	@echo
-	@echo '  ' $(RUNNERS)
-
-
-build: .merlin
-	@dune build ./test.exe
-
-man: build
-	@$(BUILD)test.exe --help
-
-run: build
-	ulimit -s $(STACK); $(BUILD)test.exe \
-		--seed $$RANDOM \
-		--timeout $(TIMEOUT) \
-		--time=$(TIME) \
-		$(addprefix --name-match ,$(ONLY)) \
-		$(addprefix --runner , $(RUNNERS))
-
-.merlin: dune
-	@dune build .merlin
-
-clean:
-	rm -rf _log _build data.csv data.csv.dat data.csv.svg data.csv.plot 
-
diff --git a/tests/suite/suite.ml b/tests/suite/suite.ml
index 5d4a0dd2c..ee9ea9314 100644
--- a/tests/suite/suite.ml
+++ b/tests/suite/suite.ml
@@ -86,7 +86,7 @@ type 'a output =
   | Done of 'a
 
 type run =
-  executable:string -> timetool:string -> timeout:float -> env:string array ->
+  executable:string -> timetool:string -> timeout:float -> env:string array -> sources:string ->
     Test.t -> result output
 
 (* Some tests are only for teyjus/elpi *)
@@ -104,7 +104,7 @@ let declare ~applicable ~run =
 type job = {
   executable : string;
   test : Test.t;
-  run : timeout:float -> env:string array -> result output;
+  run : timeout:float -> env:string array -> sources:string -> result output;
 }
 
 let (||>) l f = List.(concat (map f l))
@@ -247,18 +247,18 @@ let () = Runner.declare
     if is_elpi executable && source_elpi <> None then Runner.Can_run_it
     else Runner.Not_for_me
   end
-  ~run:begin fun ~executable ~timetool ~timeout ~env test ->
+  ~run:begin fun ~executable ~timetool ~timeout ~env ~sources test ->
   let source =
     match test.Test.source_elpi with Some x -> x | _ -> assert false in
   if not (Sys.file_exists executable) then Runner.Skipped
-  else if not (Sys.file_exists ("sources/"^source)) then Runner.Skipped
+  else if not (Sys.file_exists (sources^source)) then Runner.Skipped
   else
     let log = Util.open_log ~executable test in
     Util.write log (Printf.sprintf "executable: %s\n" executable);
 
     let { Test.expectation; input; outside_llam ; _ } = test in
-    let input = Util.option_map (fun x -> "sources/"^x) input in
-    let args = ["-test";"-no-tc";"-I";"sources";source] in
+    let input = Util.option_map (fun x -> sources^x) input in
+    let args = ["-test";"-no-tc";"-I";sources;source] in
     let args =
       if outside_llam then "-delay-problems-outside-pattern-fragment"::args
       else args in
@@ -301,16 +301,16 @@ let is_tjsim =
     if is_tjsim executable && source_teyjus <> None then Runner.Can_run_it
     else Runner.Not_for_me
   end
-  ~run:begin fun ~executable ~timetool ~timeout ~env test ->
+  ~run:begin fun ~executable ~timetool ~timeout ~env ~sources test ->
   let source =
-    match test.Test.source_teyjus with Some x -> "sources/"^x | _ -> assert false in
+    match test.Test.source_teyjus with Some x -> sources^x | _ -> assert false in
   if not (Sys.file_exists executable) then Runner.Skipped
   else if not (Sys.file_exists source) then Runner.Skipped
   else
     let log = Util.open_log ~executable test in
 
     let { Test.expectation; input; _ } = test in
-    let input = Util.option_map (fun x -> "sources/"^x) input in
+    let input = Util.option_map (fun x -> sources^x) input in
 
     let tjcc = Filename.dirname executable ^ "/tjcc" in
     let tjlink = Filename.dirname executable ^ "/tjlink" in
@@ -328,7 +328,7 @@ let is_tjsim =
       Unix.chdir old;
       dir, modname in
 
-    List.iter (fun x -> ignore (do1 tjcc ("sources/"^x)))
+    List.iter (fun x -> ignore (do1 tjcc (sources^x)))
       test.Test.deps_teyjus;
     let _ = do1 tjcc source in
 
diff --git a/tests/suite/suite.mli b/tests/suite/suite.mli
index f367fdda7..77cce627b 100644
--- a/tests/suite/suite.mli
+++ b/tests/suite/suite.mli
@@ -63,7 +63,7 @@ type 'a output =
 type job = {
   executable : string;
   test : Test.t;
-  run : timeout:float -> env:string array -> result output;
+  run : timeout:float -> env:string array -> sources:string -> result output;
 }
 
 val jobs : timetool:string -> executables:string list -> Test.t -> job list
diff --git a/tests/test.ml b/tests/test.ml
index 36b137773..b2b72cf98 100644
--- a/tests/test.ml
+++ b/tests/test.ml
@@ -51,7 +51,7 @@ let print_summary ~total ~ok ~ko ~skipped =
 
 end
 
-let run timeout _seed env { Runner.run; test; executable }  =
+let run timeout _seed sources env { Runner.run; test; executable }  =
 
   let { Test.name; description; _ } = test in
   let print = Printer.print ~executable:(Filename.basename executable) ~name ~description in
@@ -59,7 +59,7 @@ let run timeout _seed env { Runner.run; test; executable }  =
   print 0.0 0.0 0 `RUNNING;
   ANSITerminal.move_bol ();
 
-  let rc = match run ~timeout ~env with
+  let rc = match run ~timeout ~env ~sources with
     | Runner.Skipped -> print 0.0 0.0 0 `SKIPPED; None
     | Runner.Done ({ Runner.rc; _ } as x) ->
       begin match rc with
@@ -75,7 +75,7 @@ let run timeout _seed env { Runner.run; test; executable }  =
   ANSITerminal.printf [] "\n%!";
   rc
 
-let print_csv results =
+let print_csv plot results =
   let oc = open_out "data.csv" in
   results |> List.iter
     (function 
@@ -89,12 +89,12 @@ let print_csv results =
           end
       | None -> ());
   close_out oc;
-  ignore(Sys.command "./plot data.csv");
+  ignore(Sys.command (plot ^ " data.csv"));
   ignore(Sys.command "gnuplot data.csv.plot")
 ;;
 
 
-let main timeout executables namef timetool seed =
+let main sources plot timeout executables namef timetool seed =
   Random.init seed;
   let filter_name =
     let rex = Str.regexp (".*"^namef) in
@@ -107,7 +107,7 @@ let main timeout executables namef timetool seed =
     tests |> List.map (Suite.Runner.jobs ~timetool ~executables)
           |> List.concat in
   let results =
-    List.map (run timeout seed env) jobs in
+    List.map (run timeout seed sources env) jobs in
   let total, ok, ko, skipped =
     let skip, rest =
       List.partition (function None -> true | _ -> false) results in
@@ -117,7 +117,7 @@ let main timeout executables namef timetool seed =
         | _ -> false) rest in
     List.(length jobs, length ok, length ko, length skip) in
   Printer.print_summary ~total ~ok ~ko ~skipped;
-  if List.length executables > 1 then print_csv results;
+  if List.length executables > 1 then print_csv plot results;
   if ko = 0 then exit 0 else exit 1
 
 open Cmdliner
@@ -138,6 +138,14 @@ let timeout =
   let doc = "Uses $(docv) as the timeout (in seconds)." in
   Arg.(value & opt float 30.0 & info ["timeout"] ~docv:"FLOAT" ~doc)
 
+let src =
+  let doc = "Looks for the sources in $(docv)." in
+  Arg.(value & opt dir "sources/" & info ["sources"] ~docv:"DIR" ~doc)
+
+let plot =
+  let doc = "Path for the plot utility is $(docv)." in
+  Arg.(value & opt non_dir_file "./plot" & info ["plot"] ~docv:"PATH" ~doc)
+
 let mem =
   let doc = "Uses $(docv) as the tool to measure memory." in
   Arg.(value & opt non_dir_file "/usr/bin/time" & info ["time"] ~docv:"PATH" ~doc)
@@ -152,4 +160,4 @@ let info =
 ;;
 
 let () =
-  Term.exit @@ Term.eval (Term.(const main $ timeout $ runners $ namef $ mem $ seed), info)
+  Term.exit @@ Term.eval (Term.(const main $ src $ plot $ timeout $ runners $ namef $ mem $ seed), info)
diff --git a/trace/dune b/trace/dune
new file mode 100644
index 000000000..c57a34a25
--- /dev/null
+++ b/trace/dune
@@ -0,0 +1,18 @@
+(library 
+  (name trace_ppx)
+  ; (public_name trace_ppx)
+  (libraries ppx_tools_versioned ocaml-migrate-parsetree)
+  (preprocess (pps ppx_tools_versioned.metaquot_402))
+  (flags -open Ast_402)
+  (kind ppx_rewriter)
+  (ppx_runtime_libraries elpi.elpi_trace)
+  (modules trace_ppx)
+)
+
+(library 
+  (name elpi_trace)
+  (public_name elpi.elpi_trace)
+  ; (public_name trace_ppx.runtime)
+  (libraries re)
+  (modules elpi_trace)
+)
diff --git a/src/elpi_trace.ml b/trace/elpi_trace.ml
similarity index 90%
rename from src/elpi_trace.ml
rename to trace/elpi_trace.ml
index 85feb776f..66066dcf9 100644
--- a/src/elpi_trace.ml
+++ b/trace/elpi_trace.ml
@@ -3,9 +3,15 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-open Elpi_util
 module F = Format
 
+let err_fmt = ref F.err_formatter
+let set_formatter x = err_fmt := x
+let eprintf x = F.fprintf !err_fmt x
+let set_formatter_maxcols i = F.pp_set_margin !err_fmt i
+let set_formatter_maxbox i = F.pp_set_max_boxes !err_fmt i
+
+module StrMap = Map.Make(String)
 module Str = Re.Str
 
 let debug = ref false
@@ -33,7 +39,7 @@ let perf_stack = ref [{name = "main"; self = 0.0; progeny = StrMap.empty }]
 let collect_perf_enter n =
   if !collect_perf then
   match !perf_stack with
-  | { progeny } :: _ when StrMap.mem n progeny ->
+  | { progeny; _ } :: _ when StrMap.mem n progeny ->
        perf_stack := StrMap.find n progeny :: !perf_stack
   | _ ->
        perf_stack := { name = n; self = 0.0; progeny = StrMap.empty } :: !perf_stack
@@ -41,25 +47,25 @@ let collect_perf_enter n =
 let rec merge m1 m2 =
   StrMap.fold (fun _ ({ name; self; progeny } as v) m ->
      try
-       let { self = t; progeny = p } = StrMap.find name m in
+       let { self = t; progeny = p; _ } = StrMap.find name m in
        StrMap.add name { name; self = self +. t; progeny = merge progeny p } m
      with Not_found -> StrMap.add name v m) m1 m2
 
 let collect_perf_exit time =
   if !collect_perf then
   match !perf_stack with
-  | { name = n1 } as top :: ({ name = n2} as prev) :: rest when n1 = n2 ->
+  | { name = n1; _ } as top :: ({ name = n2; _ } as prev) :: rest when n1 = n2 ->
       perf_stack := { name = n2;
                       self = prev.self; 
                       progeny = merge top.progeny prev.progeny } :: rest
-  | top :: ({ progeny } as prev) :: rest ->
+  | top :: ({ progeny; _ } as prev) :: rest ->
       let top = { top with self = top.self +. time } in
       perf_stack := { prev with progeny = StrMap.add top.name top progeny } :: rest
   | _ -> assert false
 
 let rec print_tree hot { name; self; progeny } indent =
   let tprogeny, (phot, thot) =
-    StrMap.fold (fun n { self } (x,(_,m as top)) ->
+    StrMap.fold (fun n { self; _ } (x,(_,m as top)) ->
               x +. self, (if self > m then (n,self) else top))
       progeny (0.0,("",0.0)) in
   let phot =
@@ -73,7 +79,7 @@ let rec print_tree hot { name; self; progeny } indent =
 let print_perf () =
   while List.length !perf_stack > 1 do collect_perf_exit 0.0; done;
   match !perf_stack with
-  | [ { progeny } ] ->
+  | [ { progeny; _ } ] ->
         eprintf "  %-20s %s %6s %6s\n" "name"
           String.(make 20 ' ' ) "total" "self";
         eprintf "%s\n" (String.make 80 '-');
@@ -163,14 +169,14 @@ let pr_exn f = printers := f :: !printers
 
 exception TREC_CALL of Obj.t * Obj.t (* ('a -> 'b) * 'a *)
 
-let print_exit k tailcall e time =
+let print_exit tailcall e time =
   if not !trace_noprint then
     eprintf "%s}}} %s  (%.3fs)\n%!"
       (make_indent ()) (if tailcall then "->" else pr_exc e) time
 
 let exit k tailcall ?(e=OK) time =
   if condition k then begin
-    print_exit k tailcall e time;
+    print_exit tailcall e time;
     collect_perf_exit time;
   end;
   decr level
@@ -233,10 +239,10 @@ let parse_argv argv =
          only_pred := pname :: !only_pred;
          aux rest;
     | "-trace-maxbox" :: num :: rest ->
-         set_formatters_maxbox (int_of_string num);
+         set_formatter_maxbox (int_of_string num);
          aux rest
     | "-trace-maxcols" :: num :: rest ->
-         set_formatters_maxcols (int_of_string num);
+         set_formatter_maxcols (int_of_string num);
          aux rest
     | "-perf-on" :: rest ->
          collect_perf := true; on := true; trace_noprint := true; aux rest
diff --git a/src/elpi_trace.mli b/trace/elpi_trace.mli
similarity index 93%
rename from src/elpi_trace.mli
rename to trace/elpi_trace.mli
index a20ae8c50..58e806a59 100644
--- a/src/elpi_trace.mli
+++ b/trace/elpi_trace.mli
@@ -25,3 +25,6 @@ val get_cur_step : string -> int
 
 val parse_argv : string list -> string list
 val usage: string
+
+(* prints here *)
+val set_formatter : Format.formatter -> unit
diff --git a/trace_ppx.ml b/trace/trace_ppx.ml
similarity index 97%
rename from trace_ppx.ml
rename to trace/trace_ppx.ml
index 3673ee95a..6deaaa581 100644
--- a/trace_ppx.ml
+++ b/trace/trace_ppx.ml
@@ -73,8 +73,8 @@ let tcall hd args =
 let enabled = ref false
 
 let args = [
-   "--on",Arg.Set enabled,"Enable trace" ;
-   "--off",Arg.Clear enabled,"Disable trace" ;
+   "--trace_ppx-on",Arg.Set enabled,"Enable trace_ppx" ;
+   "--trace_ppx-off",Arg.Clear enabled,"Disable trace_ppx" ;
   ]
 let reset_args () =
   enabled := false
diff --git a/utils/mathpartir.sty b/utils/mathpartir.sty
deleted file mode 100644
index 6cc0f99fe..000000000
--- a/utils/mathpartir.sty
+++ /dev/null
@@ -1,492 +0,0 @@
-%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-%  Copyright (C) 2001, 2002, 2003, 2004, 2005, 2015 Didier R�my
-%
-%  Author         : Didier Remy 
-%  Version        : 1.3.0
-%  Bug Reports    : to author
-%  Web Site       : http://pauillac.inria.fr/~remy/latex/
-% 
-%  Mathpartir is free software; you can redistribute it and/or modify
-%  it under the terms of the GNU General Public License as published by
-%  the Free Software Foundation; either version 2, or (at your option)
-%  any later version.
-%  
-%  Mathpartir is distributed in the hope that it will be useful,
-%  but WITHOUT ANY WARRANTY; without even the implied warranty of
-%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-%  GNU General Public License for more details 
-%  (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
-    [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-%% \newdimen \mpr@tmpdim
-%% Dimens are a precious ressource. Uses seems to be local.
-\let \mpr@tmpdim \@tempdima
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing 
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
-  \edef \MathparNormalpar
-     {\noexpand \lineskiplimit \the\lineskiplimit
-      \noexpand \lineskip \the\lineskip}%
-  }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
-   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@cr {\penalty -10000\vadjust{\vbox{aaa}}\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
-  \let \and \mpr@andcr
-  \let \par \mpr@andcr
-  \let \\\mpr@cr
-  \let \eqno \mpr@eqno
-  \let \hva \mpr@hva
-  } 
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
-  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
-     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
-     \noindent $\displaystyle\fi
-     \MathparBindings}
-  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-\newenvironment{mathparpagebreakable}[1][]
-  {\begingroup 
-   \par
-   \mpr@savepar \parskip 0em \hsize \linewidth \centering
-      \mpr@prebindings \mpr@paroptions #1%
-      \vskip \abovedisplayskip \vskip -\lineskip%
-     \ifmmode  \else  $\displaystyle\fi
-     \MathparBindings
-  }
-  {\unskip
-   \ifmmode $\fi \par\endgroup
-   \vskip \belowdisplayskip
-   \noindent
-  \ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
-  \vbox \bgroup \tabskip 0em \let \\ \cr
-  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
-  \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
-      \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
-   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
-   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
-   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
-     \mpr@flatten \mpr@all \mpr@to \mpr@one
-     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
-     \mpr@all \mpr@stripend  
-     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
-     \ifx 1\mpr@isempty
-   \repeat
-}
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
-   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-%% Part III -- Type inference rules
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@vskip {}
-\def \mpr@htovlist {%
-   \setbox \mpr@hlist
-      \hbox {\strut
-             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
-             \unhbox \mpr@hlist}%
-   \setbox \mpr@vlist
-      \vbox {\if@premisse
-                \box \mpr@hlist
-                \ifx \mpr@vskip \empty \else
-                  \hrule height 0em depth \mpr@vskip width 0em
-                \fi
-                \unvbox \mpr@vlist
-             \else
-                \unvbox \mpr@vlist 
-                \ifx \mpr@vskip \empty \else
-                  \hrule height 0em depth \mpr@vskip width 0em
-                \fi
-                \box \mpr@hlist
-             \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-%    \setbox \mpr@hlist
-%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-%    \setbox \mpr@vlist
-%       \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
-%              \else \unvbox \mpr@vlist \box \mpr@hlist
-%              \fi}%
-% }
-
-\def \mpr@item #1{$\displaystyle #1$}
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
-  \bgroup
-  \ifx #1T\@premissetrue
-  \else \ifx #1B\@premissefalse
-  \else
-     \PackageError{mathpartir}
-       {Premisse orientation should either be T or B}
-       {Fatal error in Package}%
-  \fi \fi
-  \def \@test {#2}\ifx \@test \mpr@blank\else
-  \setbox \mpr@hlist \hbox {}%
-  \setbox \mpr@vlist \vbox {}%
-  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
-  \let \@hvlist \empty \let \@rev \empty
-  \mpr@tmpdim 0em
-  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
-  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
-  \def \\##1{%
-     \def \@test {##1}\ifx \@test \empty
-        \mpr@htovlist
-        \mpr@tmpdim 0em %%% last bug fix not extensively checked
-     \else
-      \setbox0 \hbox{\mpr@item {##1}}\relax
-      \advance \mpr@tmpdim by \wd0
-      %\mpr@tmpdim 1.02\mpr@tmpdim
-      \ifnum \mpr@tmpdim < \hsize
-         \ifnum \wd\mpr@hlist > 0
-           \if@premisse
-             \setbox \mpr@hlist 
-                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
-           \else
-             \setbox \mpr@hlist
-                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
-           \fi
-         \else 
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-         \fi
-      \else
-         \ifnum \wd \mpr@hlist > 0
-            \mpr@htovlist 
-            \mpr@tmpdim \wd0
-         \fi
-         \setbox \mpr@hlist \hbox {\unhbox0}%
-      \fi
-      \advance \mpr@tmpdim by \mpr@sep
-   \fi
-   }%
-   \@rev
-   \mpr@htovlist
-   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
-   \fi
-   \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
-    \let\@@over\over % fallback if amsmath is not loaded
-    \let\@@overwithdelims\overwithdelims
-    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
-    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
-  }{}
-
-%% The default
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\mpr@over #2}$}}
-\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
-    $\displaystyle {#1\@@atop #2}$}}
-
-\let \mpr@fraction \mpr@@fraction
-
-%% A generic solution to arrow
-
-\def \mpr@@fractionaboveskip {0ex}
-\def \mpr@@fractionbelowskip {0.22ex}
-
-\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
-     \def \mpr@tail{#1}%
-     \def \mpr@body{#2}%
-     \def \mpr@head{#3}%
-     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
-     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
-     \dimen0\ht3\advance\dimen0 by \dp3\relax
-     \dimen0 0.5\dimen0\relax
-     \advance \dimen0 by \mpr@@fractionaboveskip
-     \setbox1=\hbox {\raise \dimen0 \box1}\relax
-     \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
-     \advance \dimen0 by \mpr@@fractionbelowskip
-     \setbox2=\hbox {\lower \dimen0 \box2}\relax
-     \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
-     \dimen0=\wd0\box0
-     \box0 \hskip -\dimen0\relax
-     \hbox to \dimen0 {$%\color{blue}
-       \mathrel{\mpr@tail}\joinrel
-       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
-     $}}}
-
-%% Old stuff should be removed in next version
-\def \mpr@@nothing #1#2
-    {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
-\def \mpr@@reduce #1#2{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
-    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
-  {\bgroup
-     \ifnum \linewidth<\hsize \hsize \linewidth\fi
-     \mpr@rulelineskip
-     \let \and \qquad
-     \let \hva \mpr@hva
-     \let \@rulename \mpr@empty
-     \let \@rule@options \mpr@empty
-     \let \mpr@over \@@over
-     \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
-  {\everymath={\displaystyle}%       
-   \def \@test {#2}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
-   \else 
-   \def \@test {#3}\ifx \empty \@test
-      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
-   \else
-   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
-   \fi \fi
-   \def \@test {#1}\ifx \@test\empty \box0
-   \else \vbox 
-%%% Suggestion de Francois pour les etiquettes longues
-%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
-      {\hbox {\DefTirName {#1}}\box0}\fi
-   \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible, 
-% and  vertical breaks if needed. 
-% 
-% An empty element obtained by \\\\ produces a vertical break in all cases. 
-%
-% The former rule is aligned on the fraction bar. 
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-% 
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%       
-%  width                set the width of the rule to val
-%  narrower             set the width of the rule to val\hsize
-%  before               execute val at the beginning/left
-%  lab                  put a label [Val] on top of the rule
-%  lskip                add negative skip on the right
-%  left                 put a left label [Val]
-%  Left                 put a left label [Val],  ignoring its width 
-%  right                put a right label [Val]
-%  Right                put a right label [Val], ignoring its width
-%  leftskip             skip negative space on the left-hand side
-%  rightskip            skip negative space on the right-hand side
-%  vdots                lift the rule by val and fill vertical space with dots
-%  after                execute val at the end/right
-%  
-%  Note that most options must come in this order to avoid strange
-%  typesetting (in particular  leftskip must preceed left and Left and
-%  rightskip must follow Right or right; vdots must come last 
-%  or be only followed by rightskip. 
-%  
-
-%% Keys that make sence in all kinds of rules
-\def \mprset #1{\setkeys{mprset}{#1}}
-\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
-\define@key {mprset}{lineskip}[]{\lineskip=#1}
-\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
-\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-% To be documented.
-\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
-\define@key {mprset}{sep}{\def\mpr@sep{#1}}
-\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
-\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
-\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def}
-\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
-\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
-\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
-\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def}
-\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
-\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
-\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
-     \advance \hsize by -\wd0\box0}
-
-\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
-     \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
-\define@key {mpr}{right}
-  {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
-  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
-   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
-  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}
-
-\newif \ifmpr@vcenter \mpr@vcenterfalse
-\newcommand \mpr@inferstar@ [3][]{\begingroup
-  \setbox0 \hbox
-        {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
-         \setbox \mpr@right \hbox{}%
-         \setkeys{mpr}{#1}%
-         $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
-          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
-          \box \mpr@right \mpr@vdots$
-          \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
-  \ifmpr@vcenter
-     \box0
-  \else 
-     \setbox1 \hbox {\strut}  
-     \@tempdima \dp0 \advance \@tempdima by -\dp1
-     \raise \@tempdima \box0
-  \fi
-  \endgroup}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode 
-    \let \@do \mpr@inferstar@
-  \else 
-    \let \@do \mpr@err@skipargs
-    \PackageError {mathpartir}
-      {\string\inferrule* can only be used in math mode}{}%
-  \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \TirNameStyle #1{\small \textsc{#1}}
-\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
-\def \RightTirNameStyle #1{\TirNameStyle {#1}}
-
-\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
-\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
-\let \TirName \lefttir@name
-\let \LeftTirName \lefttir@name
-\let \DefTirName \lefttir@name
-\let \LabTirName \lefttir@name
-\let \RightTirName \righttir@name
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput