diff --git a/dune-project b/dune-project
index 59f4ed39ea3f90ecfa220272a2eb34f79eddbcb6..53b708f43595f4c9ba4486c7a37c43d9d333d16a 100644
--- a/dune-project
+++ b/dune-project
@@ -36,5 +36,3 @@
            ("ocaml" (>= "4.08"))
          )
 )
-
-(formatting disabled)
diff --git a/src/bin/dune b/src/bin/dune
index 8fe364ef536521048bf62b0c2c5eb33b35f7e324..6a9f7aa3710a997f5afb601712978ff09d9fc519 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -1,27 +1,33 @@
 (executable
-  (name           main)
-  (public_name    colibrics)
-  (libraries
-    ; external deps
-    cmdliner fmt gen
-    ; dolmen deps
-    dolmen dolmen.intf dolmen.std
-    dolmen_type dolmen_loop
-    ; colibrics
-    colibrics
-  )
-   (package colibrics)
-)
+ (name main)
+ (public_name colibrics)
+ (libraries
+  ; external deps
+  cmdliner
+  fmt
+  gen
+  ; dolmen deps
+  dolmen
+  dolmen.intf
+  dolmen.std
+  dolmen_type
+  dolmen_loop
+  ; colibrics
+  colibrics)
+ (package colibrics))
 
 ; Rule to generate a man page for colibrics
+
 (rule
-  (target        colibrics.1)
-  (action (with-outputs-to %{target} (run colibrics --help=groff)))
-)
+ (target colibrics.1)
+ (action
+  (with-outputs-to
+   %{target}
+   (run colibrics --help=groff))))
 
 ; Install the man page
+
 (install
- (files    colibrics.1)
- (section  man)
- (package  colibrics)
-)
+ (files colibrics.1)
+ (section man)
+ (package colibrics))
diff --git a/src/lib/constraints/dune b/src/lib/constraints/dune
index 71675cb550bb51a3bad5737d7b50e3479b0d04d5..27671d52b611fefbf202be1dad7602c8a15f0cc1 100644
--- a/src/lib/constraints/dune
+++ b/src/lib/constraints/dune
@@ -1,12 +1,14 @@
 (rule
  (targets simple.mlw)
- (action (run generator/generate_simple.exe %{dep:constraints.json} %{dep:simple.template.mlw} simple.mlw))
-)
+ (action
+  (run generator/generate_simple.exe %{dep:constraints.json}
+    %{dep:simple.template.mlw} simple.mlw)))
 
 (rule
  (targets dune.generated)
- (action (run generator/generate_simple.exe %{dep:constraints.json} %{dep:dune.template.generated} dune.generated))
-  (mode promote)
-)
+ (action
+  (run generator/generate_simple.exe %{dep:constraints.json}
+    %{dep:dune.template.generated} dune.generated))
+ (mode promote))
 
 (include dune.generated)
diff --git a/src/lib/constraints/generator/dune b/src/lib/constraints/generator/dune
index 89da57b37da2a342ff57dcc07f873f6a2a19c15d..cf673623db4fe74e53e90e782a241624236aab0a 100644
--- a/src/lib/constraints/generator/dune
+++ b/src/lib/constraints/generator/dune
@@ -1,5 +1,5 @@
 (executable
  (name generate_simple)
- (preprocess (pps ppx_deriving_yojson))
- (libraries jingoo yojson logs core)
-)
+ (preprocess
+  (pps ppx_deriving_yojson))
+ (libraries jingoo yojson logs core))
diff --git a/src/lib/dune b/src/lib/dune
index c96b84f60708f9a84b74aa91497b9eabbda825c4..58f4640d14ac61c27f6ac12f9a4a9e675c31739f 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -1,14 +1,20 @@
 (library
-        (public_name colibrics)
-        (libraries zarith)
-       (flags (-w -3))
-)
+ (public_name colibrics)
+ (libraries zarith)
+ (flags
+  (-w -3)))
 
 (rule
-   (deps cp.mlw all.mlw utils/tagtbl.mlw utils/extstd.mlw cp.drv constraints/simple.mlw)
-   (targets utils__extstd__Int63.ml utils__extstd__Bool.ml cp__Impl0.ml cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml constraints__simple__Simple.ml cp__ConstraintHelpers.ml all__All.ml all__API.ml all__APIDefensive.ml)
-   (action (run why3 extract -L . -D ocaml64 -D cp.drv -o . --modular
-     utils.extstd.Int63 utils.extstd.Bool cp.Impl0 cp.Var cp.Var0 cp.Type cp.DomI cp.DomB constraints.simple.Simple cp.ConstraintHelpers all.All all.API all.APIDefensive))
-)
+ (deps cp.mlw all.mlw utils/tagtbl.mlw utils/extstd.mlw cp.drv
+   constraints/simple.mlw)
+ (targets utils__extstd__Int63.ml utils__extstd__Bool.ml cp__Impl0.ml
+   cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml
+   constraints__simple__Simple.ml cp__ConstraintHelpers.ml all__All.ml
+   all__API.ml all__APIDefensive.ml)
+ (action
+  (run why3 extract -L . -D ocaml64 -D cp.drv -o . --modular
+    utils.extstd.Int63 utils.extstd.Bool cp.Impl0 cp.Var cp.Var0 cp.Type
+    cp.DomI cp.DomB constraints.simple.Simple cp.ConstraintHelpers all.All
+    all.API all.APIDefensive)))
 
 (copy_files constraints/*.ml)
diff --git a/src_colibri2/bin/dune b/src_colibri2/bin/dune
index 6e100b5c6a298e13b4614bc8b246b927cdac0f87..08e03bf225673d995285268e8f613c839ab0cc5d 100644
--- a/src_colibri2/bin/dune
+++ b/src_colibri2/bin/dune
@@ -1,31 +1,37 @@
 (executable
-  (name           main)
-  (public_name    colibri2)
-  (flags -linkall)
-  (libraries
-    ; external deps
-    cmdliner fmt gen
-    ; dolmen deps
-    dolmen dolmen.intf dolmen.std
-    dolmen_type dolmen_loop
-    ; colibrics
-    colibri2.solver
-    colibri2.theories.bool
-    colibri2.theories.LRA
-    colibri2.theories.quantifiers
-  )
-   (package colibri2)
-)
+ (name main)
+ (public_name colibri2)
+ (flags -linkall)
+ (libraries
+  ; external deps
+  cmdliner
+  fmt
+  gen
+  ; dolmen deps
+  dolmen
+  dolmen.intf
+  dolmen.std
+  dolmen_type
+  dolmen_loop
+  ; colibrics
+  colibri2.solver
+  colibri2.theories.bool
+  colibri2.theories.LRA
+  colibri2.theories.quantifiers)
+ (package colibri2))
 
 ; Rule to generate a man page for colibrics
+
 (rule
-  (target        colibri2.1)
-  (action (with-outputs-to %{target} (run colibri2 --help=groff)))
-)
+ (target colibri2.1)
+ (action
+  (with-outputs-to
+   %{target}
+   (run colibri2 --help=groff))))
 
 ; Install the man page
+
 (install
- (files    colibri2.1)
- (section  man)
- (package  colibri2)
-)
+ (files colibri2.1)
+ (section man)
+ (package colibri2))
diff --git a/src_colibri2/core/structures/dune b/src_colibri2/core/structures/dune
index c2f3e18faf340f3934b26c31038322308be0705e..ea68cfe709676bb1153ab933d3dcac0a154853de 100644
--- a/src_colibri2/core/structures/dune
+++ b/src_colibri2/core/structures/dune
@@ -3,7 +3,8 @@
  (public_name colibri2.core.structures)
  (synopsis
    "core structures for colibri2, e.g. terms, semantic terms, values, etc")
- (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib str dolmen.std)
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib str
+   dolmen.std)
  (preprocess
   (pps ppx_deriving.std))
  (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
diff --git a/src_colibri2/popop_lib/dune b/src_colibri2/popop_lib/dune
index e87b7191d643bd2e23e1035bff4a5895d7c6b722..e668e715828128044b83a34aad71016b0eaf25b2 100644
--- a/src_colibri2/popop_lib/dune
+++ b/src_colibri2/popop_lib/dune
@@ -3,7 +3,8 @@
 (library
  (name colibri2_popop_lib)
  (public_name colibri2.popop_lib)
- (synopsis "Temporary for colibri2 (intended to be replaced by another library)")
+ (synopsis
+   "Temporary for colibri2 (intended to be replaced by another library)")
  (libraries str unix zarith base fmt)
  (preprocess
   (pps ppx_deriving.std ppx_hash))
diff --git a/src_colibri2/solver/dune b/src_colibri2/solver/dune
index ec643c4a3565c7bd51936a0353e2dda9694d290c..1f81076c7215f68f1ad55c0ed2021e63ddf150bb 100644
--- a/src_colibri2/solver/dune
+++ b/src_colibri2/solver/dune
@@ -3,7 +3,8 @@
  (public_name colibri2.solver)
  (synopsis "colibri2's solver")
  (libraries containers zarith ocamlgraph gen dolmen spelll colibri2.stdlib
-   colibri2.popop_lib str colibri2.core colibri2.core.structures dolmen_loop dolmen_type)
+   colibri2.popop_lib str colibri2.core colibri2.core.structures dolmen_loop
+   dolmen_type)
  (preprocess
   (pps ppx_deriving.std))
  (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
diff --git a/src_colibri2/tests/dune b/src_colibri2/tests/dune
index 7695ec893c847a0506a979fdddc5d76d9891a26d..2e1a6fd8e25b86b12644c93a8842a4122385e3f7 100644
--- a/src_colibri2/tests/dune
+++ b/src_colibri2/tests/dune
@@ -1,15 +1,14 @@
 (executable
  (modes byte exe)
  (name tests)
- (libraries containers colibri2.core colibri2.theories.bool colibri2.theories.LRA
-   ounit2 colibri2.solver colibri2.stdlib)
+ (libraries containers colibri2.core colibri2.theories.bool
+   colibri2.theories.LRA ounit2 colibri2.solver colibri2.stdlib)
  (flags :standard -w +a-4-42-44-48-50-58-32-60-9@8 -color always)
  (ocamlopt_flags :standard -O3 -unbox-closures -unbox-closures-factor 20))
 
 (rule
  (alias runtest)
  (deps
-  (:< tests.exe)
- )
+  (:< tests.exe))
  (action
   (run %{<})))
diff --git a/src_colibri2/tests/generate_tests/dune b/src_colibri2/tests/generate_tests/dune
index 1d7c405ab1f2488562b00be79164024fce522079..b98d6cdc574641ee1550f528627b9c65975fbb30 100644
--- a/src_colibri2/tests/generate_tests/dune
+++ b/src_colibri2/tests/generate_tests/dune
@@ -1,3 +1,2 @@
 (executable
- (name generate_dune_tests)
-)
+ (name generate_dune_tests))
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune b/src_colibri2/tests/solve/dimacs/sat/dune
index 47c20f59db19181b6fa81ba0b8d9d7e956ce111f..87aec8cee7b54a9b5770453bb688a103592210ab 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune
+++ b/src_colibri2/tests/solve/dimacs/sat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune b/src_colibri2/tests/solve/dimacs/unsat/dune
index 9ca94f8953f83cc072987091ba8429012ab24703..959922d115ac3b89aec38904a6221b2730b37e08 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune b/src_colibri2/tests/solve/smt_lra/sat/dune
index 47c20f59db19181b6fa81ba0b8d9d7e956ce111f..87aec8cee7b54a9b5770453bb688a103592210ab 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune b/src_colibri2/tests/solve/smt_lra/unsat/dune
index 9ca94f8953f83cc072987091ba8429012ab24703..959922d115ac3b89aec38904a6221b2730b37e08 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune b/src_colibri2/tests/solve/smt_quant/sat/dune
index 47c20f59db19181b6fa81ba0b8d9d7e956ce111f..87aec8cee7b54a9b5770453bb688a103592210ab 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune b/src_colibri2/tests/solve/smt_quant/unsat/dune
index 9ca94f8953f83cc072987091ba8429012ab24703..959922d115ac3b89aec38904a6221b2730b37e08 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune b/src_colibri2/tests/solve/smt_uf/sat/dune
index 47c20f59db19181b6fa81ba0b8d9d7e956ce111f..87aec8cee7b54a9b5770453bb688a103592210ab 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune b/src_colibri2/tests/solve/smt_uf/unsat/dune
index 9ca94f8953f83cc072987091ba8429012ab24703..959922d115ac3b89aec38904a6221b2730b37e08 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune
@@ -2,7 +2,11 @@
 
 (rule
  (alias runtest)
- (deps (glob_files *.cnf) (glob_files *.smt2))
- (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
- (mode promote)
-)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/theories/LRA/dune b/src_colibri2/theories/LRA/dune
index 0dade57c5cf443398ec7916c8b74b9404bdb5e8c..69c7f9f02a07b9a6c7361a14ca43ffe562522272 100644
--- a/src_colibri2/theories/LRA/dune
+++ b/src_colibri2/theories/LRA/dune
@@ -5,8 +5,7 @@
  (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
    colibri2.core.structures colibri2.core colibri2.theories.bool)
  (preprocess
-  (pps ppx_deriving.std ppx_hash
- ))
+  (pps ppx_deriving.std ppx_hash))
  (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
    Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
    Colibri2_theories_bool)
diff --git a/src_colibri2/theories/quantifier/dune b/src_colibri2/theories/quantifier/dune
index 09adaaec9425c4ac01b91c98e0bbb56882d97c79..dbf85cf3e97adb77fa34de14c856ad6861b51827 100644
--- a/src_colibri2/theories/quantifier/dune
+++ b/src_colibri2/theories/quantifier/dune
@@ -6,8 +6,7 @@
    colibri2.core.structures colibri2.core colibri2.theories.bool)
  (preprocess
   (pps ppx_deriving.std ppx_hash))
- (flags :standard -open
-   Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
-   Colibri2_theories_bool)
+ (flags :standard -open Containers -open Colibri2_stdlib -open Std -open
+   Colibri2_core -open Colibri2_theories_bool)
  (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
    -unbox-closures-factor 20))
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 3237bf423fed8f51d8cc8cfd24d3d367523ebdba..50bdd9135d27bdb62de47ccf0fc01c55d17ee52e 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -4,7 +4,8 @@ open Colibri2_popop_lib
 open Colibri2_core
 module F = Expr.Term.Const
 
-let debug = Debug.register_info_flag ~desc:"Handling of quantifiers" "quantifiers"
+let debug =
+  Debug.register_info_flag ~desc:"Handling of quantifiers" "quantifiers"
 
 (** instantiated function symbol *)
 module FA = struct
@@ -55,80 +56,84 @@ module Info = struct
     parents : Node.S.t F_Pos.M.t;  (** parents *)
     apps : Ground.S.t F.M.t;  (** parent parent *)
     tys : Ground.Ty.S.t;
-  } [@@deriving show]
+  }
+  [@@deriving show]
 
   let _ = pp
 
-  let merge info info' = {
-    parents = F_Pos.M.union (fun _ a b -> Some (Node.S.union a b)) info.parents info'.parents;
-    apps = F.M.union (fun _ a b -> Some (Ground.S.union a b)) info.apps info'.apps;
-    tys = Ground.Ty.S.union info.tys info'.tys;
-  }
+  let merge info info' =
+    {
+      parents =
+        F_Pos.M.union
+          (fun _ a b -> Some (Node.S.union a b))
+          info.parents info'.parents;
+      apps =
+        F.M.union (fun _ a b -> Some (Ground.S.union a b)) info.apps info'.apps;
+      tys = Ground.Ty.S.union info.tys info'.tys;
+    }
 
-  let empty = {
-    parents = F_Pos.M.empty;
-    apps = F.M.empty;
-    tys = Ground.Ty.S.empty;
-  }
+  let empty =
+    { parents = F_Pos.M.empty; apps = F.M.empty; tys = Ground.Ty.S.empty }
 
   let env =
-    Datastructure.HNode.create (Fmt.nop:t Format.printer) "Quantifier.info"
-
+    Datastructure.HNode.create (Fmt.nop : t Format.printer) "Quantifier.info"
 end
 
 module PC = struct
   module T = struct
     open! Base
+
     type t = { parent : F_Pos.t; child : F.t }
     [@@deriving show, ord, hash, show, eq]
   end
+
   include T
   include Popop_stdlib.MkDatatype (T)
-
 end
 
 module PP = struct
   module T = struct
     open! Base
-    type t =  { parent1 : F_Pos.t; parent2 : F_Pos.t }
+
+    type t = { parent1 : F_Pos.t; parent2 : F_Pos.t }
     [@@deriving show, ord, hash, show, eq]
   end
+
   include T
   include Popop_stdlib.MkDatatype (T)
 
   let create p1 p2 =
-    if F_Pos.compare p1 p2 <= 0
-    then { parent1 = p1; parent2 = p2 }
+    if F_Pos.compare p1 p2 <= 0 then { parent1 = p1; parent2 = p2 }
     else { parent1 = p1; parent2 = p2 }
-
 end
 
 module Pattern = struct
   module T = struct
     open Base
 
-    type t =
-      | Var of Expr.Term.Var.t
-      | App of F.t * Expr.Ty.t list * t list
+    type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
     [@@deriving eq, ord, hash]
 
     let rec pp fmt = function
       | Var v -> Expr.Term.Var.pp fmt v
-      | App (f,tyl,tl) ->
-        Fmt.pf fmt "%a[%a](%a)"
-          F.pp f
-          Fmt.(list ~sep:comma Expr.Ty.pp) tyl
-          Fmt.(list ~sep:comma pp) tl
+      | App (f, tyl, tl) ->
+          Fmt.pf fmt "%a[%a](%a)" F.pp f
+            Fmt.(list ~sep:comma Expr.Ty.pp)
+            tyl
+            Fmt.(list ~sep:comma pp)
+            tl
   end
 
   include T
   include Popop_stdlib.MkDatatype (T)
 
-  let rec of_term (t:Expr.Term.t) =
+  let rec of_term (t : Expr.Term.t) =
     match t.descr with
     | Var v -> Var v
-    | App (f,tys,tl) -> App(f,tys,List.map of_term tl)
-    | _ -> assert false (* absurd *)
+    | App (f, tys, tl) -> App (f, tys, List.map of_term tl)
+    | _ -> assert false
+
+  (* absurd *)
 
   let rec fold2_result f acc l l' =
     match (l, l') with
@@ -146,203 +151,219 @@ module Pattern = struct
         | exception Not_found -> Ok (Expr.Ty.Var.M.add v ty sty)
         | ty' -> if Ground.Ty.equal ty ty' then Ok sty else Error () )
     | App (cst', tyl') ->
-      if Expr.Ty.Const.equal ty.app cst'
-      then fold2_result match_ty sty ty.args tyl'
+        if Expr.Ty.Const.equal ty.app cst' then
+          fold2_result match_ty sty ty.args tyl'
         else Error ()
 
-  let rec match_term d (seq: Ground.Subst.t Seq.t) (n : Node.t) (p : t)
-    : Ground.Subst.t Seq.t =
+  let rec match_term d (seq : Ground.Subst.t Seq.t) (n : Node.t) (p : t) :
+      Ground.Subst.t Seq.t =
     Debug.dprintf4 debug "[Quant] matching %a %a" pp p Node.pp n;
     let open Seq.Infix in
     match p with
     | Var v -> (
         seq >>= fun subst ->
-        let match_ty (acc:_ list) ty : Ground.Subst.t list =
+        let match_ty (acc : _ list) ty : Ground.Subst.t list =
           match match_ty subst.ty ty v.ty with
           | Error () -> acc
           | Ok sty -> (
               match Expr.Term.Var.M.find v subst.term with
               | exception Not_found ->
-                { term = Expr.Term.Var.M.add v n subst.term; ty = sty }::acc
+                  { term = Expr.Term.Var.M.add v n subst.term; ty = sty } :: acc
               | n' ->
-                if Egraph.is_equal d n n' then
-                  { term = subst.term; ty = sty }::acc
-                else acc)
+                  if Egraph.is_equal d n n' then
+                    { term = subst.term; ty = sty } :: acc
+                  else acc )
         in
         match Datastructure.HNode.find_opt Info.env d n with
         | None -> Seq.empty
-        | Some info ->
-          Seq.of_list (Ground.Ty.S.fold_left match_ty [] info.tys)
-
-      )
+        | Some info -> Seq.of_list (Ground.Ty.S.fold_left match_ty [] info.tys)
+        )
     | App (pf, ptyl, pargs) ->
-      let s = Opt.get_def Ground.S.empty @@
+        let s =
+          Opt.get_def Ground.S.empty
+          @@
           let open Option in
-          let* info = Datastructure.HNode.find_opt Info.env d
-              (Egraph.find_def d n) in
+          let* info =
+            Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n)
+          in
           F.M.find_opt pf info.apps
-      in
-      (* to remove *)
-        seq >>= fun {term=st;ty=sty} ->
+        in
+        (* to remove *)
+        seq >>= fun { term = st; ty = sty } ->
         Ground.S.fold_left
           (fun acc n ->
-            let {Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
-                assert (Term.Const.equal f pf);
-                match fold2_result match_ty sty tyl ptyl with
-                | Error () -> acc
-                | Ok sty ->
-                    Seq.append acc (fun () ->
-                        let seq =
-                          Base.List.fold2_exn args pargs
-                            ~init:(Seq.singleton {Ground.Subst.term = st; ty = sty})
-                            ~f:(fun acc arg parg ->
-                                match_term d acc arg parg)
-                        in
-                        seq ())
-          ) Seq.empty s
+            let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
+            assert (Term.Const.equal f pf);
+            match fold2_result match_ty sty tyl ptyl with
+            | Error () -> acc
+            | Ok sty ->
+                Seq.append acc (fun () ->
+                    let seq =
+                      Base.List.fold2_exn args pargs
+                        ~init:
+                          (Seq.singleton { Ground.Subst.term = st; ty = sty })
+                        ~f:(fun acc arg parg -> match_term d acc arg parg)
+                    in
+                    seq ()))
+          Seq.empty s
 
   let get_pps pattern =
     let rec aux acc fp p =
       match p with
-      | Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
-      | App(f,_,tl) ->
-        List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
+      | Var v ->
+          Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
+      | App (f, _, tl) ->
+          List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
     in
-    let m = match pattern with
+    let m =
+      match pattern with
       | Var _ -> Expr.Term.Var.M.empty
-      | App(f,_,tl) ->
-        List.foldi
-          (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
-          Expr.Term.Var.M.empty tl
+      | App (f, _, tl) ->
+          List.foldi
+            (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
+            Expr.Term.Var.M.empty tl
     in
-    Expr.Term.Var.M.map (fun s ->
+    Expr.Term.Var.M.map
+      (fun s ->
         let l = F_Pos.S.elements s in
-        Lists.fold_product (fun acc parents1 parents2 ->
+        Lists.fold_product
+          (fun acc parents1 parents2 ->
             if F_Pos.equal parents1 parents2 then acc
-            else (PP.create parents1 parents2)::acc
-          ) [] l l) m
-
+            else PP.create parents1 parents2 :: acc)
+          [] l l)
+      m
 end
 
 module Trigger = struct
   module T = struct
     open! Base
 
-    type t = { pat : Pattern.t (* list *); form : Ground.ThClosedQuantifier.t }
+    type t = { pat : Pattern.t; (* list *) form : Ground.ThClosedQuantifier.t }
     [@@deriving eq, ord, hash]
 
-    let pp fmt t = Fmt.pf fmt "[%a -> %a]" Pattern.pp t.pat Ground.ThClosedQuantifier.pp t.form
+    let pp fmt t =
+      Fmt.pf fmt "[%a -> %a]" Pattern.pp t.pat Ground.ThClosedQuantifier.pp
+        t.form
   end
 
   include T
   include Popop_stdlib.MkDatatype (T)
 
-  let compute_triggers (cq:Ground.ThClosedQuantifier.t) =
+  let compute_triggers (cq : Ground.ThClosedQuantifier.t) =
     let cq' = Ground.ThClosedQuantifier.sem cq in
     let tyvs = cq'.ty_vars in
     let tvs = cq'.term_vars in
     let t = cq'.body in
-    let union (sty,st) = function
+    let union (sty, st) = function
       | None -> None
-      | Some (sty',st') ->
-        Some (Expr.Ty.Var.S.union sty sty',
-              Expr.Term.Var.S.union st st')
-    in
-    let add t fv pats =
-      (t,fv)::pats
+      | Some (sty', st') ->
+          Some (Expr.Ty.Var.S.union sty sty', Expr.Term.Var.S.union st st')
     in
-    let rec aux (pats,acc_fv) (t:Expr.Term.t) =
+    let add t fv pats = (t, fv) :: pats in
+    let rec aux (pats, acc_fv) (t : Expr.Term.t) =
       match t.descr with
       | Var _ ->
-        let fv = Expr.Term.free_vars (Expr.Ty.Var.S.empty,Expr.Term.Var.S.empty) t in
-        add t fv pats, union fv acc_fv
-      | Expr.App (_, tyl, tl) -> begin
-        let pats, fv =
-          List.fold_left aux
-            (pats,(Some (Expr.Ty.Var.S.empty,Expr.Term.Var.S.empty)))
-            tl
-        in
-        match fv with
-        | None -> (pats, None)
-        | Some (sty,st) ->
-          let fv = (List.fold_left Expr.Ty.free_vars sty tyl,st) in
-          add t fv pats, union fv acc_fv
-      end
-      | Expr.Binder (_, _) -> pats,None (* todo *)
-      | Expr.Match (_, _) -> pats,None (* todo *)
+          let fv =
+            Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) t
+          in
+          (add t fv pats, union fv acc_fv)
+      | Expr.App (_, tyl, tl) -> (
+          let pats, fv =
+            List.fold_left aux
+              (pats, Some (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty))
+              tl
+          in
+          match fv with
+          | None -> (pats, None)
+          | Some (sty, st) ->
+              let fv = (List.fold_left Expr.Ty.free_vars sty tyl, st) in
+              (add t fv pats, union fv acc_fv) )
+      | Expr.Binder (_, _) -> (pats, None) (* todo *)
+      | Expr.Match (_, _) -> (pats, None)
+      (* todo *)
     in
-    let pats, _ = aux ([],None) t in
+    let pats, _ = aux ([], None) t in
     let tyvs = Expr.Ty.Var.S.of_list tyvs in
     let tvs = Expr.Term.Var.S.of_list tvs in
-    let pats = List.filter_map (fun (c,(sty,st)) ->
-        if Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs then
-          Some { pat = Pattern.of_term c; form = cq }
-        else None
-      ) pats in
+    let pats =
+      List.filter_map
+        (fun (c, (sty, st)) ->
+          if Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs then
+            Some { pat = Pattern.of_term c; form = cq }
+          else None)
+        pats
+    in
     pats
 
   let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
-  module EnvApps = Datastructure.Memo(F)
+
+  module EnvApps = Datastructure.Memo (F)
+
   let env_apps =
     EnvApps.create
       (Context.Queue.pp ~sep:Fmt.semi pp)
-      "Quantifier.Trigger.apps"
-      Context.Queue.create
+      "Quantifier.Trigger.apps" Context.Queue.create
 
   let add_trigger d t =
     match t.pat with
     | Var _ -> Datastructure.Queue.push env_vars d t
-    | App(f,_,_) -> Context.Queue.push (EnvApps.find env_apps d f) t
+    | App (f, _, _) -> Context.Queue.push (EnvApps.find env_apps d f) t
 
   let match_ d tri n =
     Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
-    let mvar = Pattern.match_term d (Seq.singleton Ground.Subst.empty) n tri.pat in
-    Seq.iter (fun subst ->
+    let mvar =
+      Pattern.match_term d (Seq.singleton Ground.Subst.empty) n tri.pat
+    in
+    Seq.iter
+      (fun subst ->
         Debug.dprintf2 debug "[Quant] %a match found" Ground.Subst.pp subst;
-        let n = Ground.convert ~subst (Ground.ThClosedQuantifier.sem tri.form).body in
+        let n =
+          Ground.convert ~subst (Ground.ThClosedQuantifier.sem tri.form).body
+        in
         Egraph.register d n;
-        Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form)) mvar
+        Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form))
+      mvar
 end
 
 module InvertedPath = struct
-
   type t = {
-    patterns: Trigger.t list Context.Ref.t;
-    apps: t F_Pos.M.t Context.Ref.t;
+    patterns : Trigger.t list Context.Ref.t;
+    apps : t F_Pos.M.t Context.Ref.t;
   }
 
-  let create creator = {
-    patterns = Context.Ref.create creator [];
-    apps = Context.Ref.create creator F_Pos.M.empty;
-  }
+  let create creator =
+    {
+      patterns = Context.Ref.create creator [];
+      apps = Context.Ref.create creator F_Pos.M.empty;
+    }
 
   let rec walk d acc n t =
     let acc =
-        List.fold_left
-          (fun acc p ->
-            Trigger.M.add_change Node.S.singleton Node.S.add p n acc)
-          acc (Context.Ref.get t.patterns)
+      List.fold_left
+        (fun acc p -> Trigger.M.add_change Node.S.singleton Node.S.add p n acc)
+        acc
+        (Context.Ref.get t.patterns)
     in
-    let info =
-      Datastructure.HNode.find_opt Info.env d
-        (Egraph.find_def d n) in
+    let info = Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n) in
     match info with
     | None -> acc (* a class without term associated, can't be matched *)
     | Some info ->
-      F_Pos.M.fold_left
-        (fun acc p x ->
-           Node.S.fold_left
-             (fun acc n -> walk d acc n x)
-             acc
-             (F_Pos.M.find p info.parents))
-        acc (Context.Ref.get t.apps)
-
-  module HPC = Datastructure.Memo(PC)
-  module HPP = Datastructure.Memo(PP)
-  module HPT = Datastructure.Memo(F_Pos)
+        F_Pos.M.fold_left
+          (fun acc p x ->
+            Node.S.fold_left
+              (fun acc n -> walk d acc n x)
+              acc
+              (F_Pos.M.find p info.parents))
+          acc (Context.Ref.get t.apps)
+
+  module HPC = Datastructure.Memo (PC)
+  module HPP = Datastructure.Memo (PP)
+  module HPT = Datastructure.Memo (F_Pos)
 
   let pc_ips = HPC.create Fmt.nop "Quantifier.pc" create
+
   let pp_ips = HPP.create Fmt.nop "Quantifier.pp" create
+
   let pt_ips = HPT.create Fmt.nop "Quantifier.pt" Context.Queue.create
 
   let get_fp d ip fp =
@@ -350,74 +371,84 @@ module InvertedPath = struct
     match F_Pos.M.find_opt fp m with
     | Some ip -> ip
     | None ->
-      let ip = create (Egraph.context d) in
-      let m = F_Pos.M.add fp ip m in
-      Context.Ref.set ip.apps m;
-      ip
+        let ip = create (Egraph.context d) in
+        let m = F_Pos.M.add fp ip m in
+        Context.Ref.set ip.apps m;
+        ip
 
   let add_pattern ip pat =
-    Context.Ref.set ip.patterns (pat::(Context.Ref.get ip.patterns))
+    Context.Ref.set ip.patterns (pat :: Context.Ref.get ip.patterns)
 
-  let insert_pattern d (trigger:Trigger.t) =
-    let rec aux (fp:F_Pos.t) pp_vars p =
+  let insert_pattern d (trigger : Trigger.t) =
+    let rec aux (fp : F_Pos.t) pp_vars p =
       match p with
-      | Pattern.Var v -> begin
+      | Pattern.Var v ->
           let b = Expr.Term.Var.M.find_def [] v pp_vars in
-          let b = List.filter
-              (fun pp -> F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
+          let b =
+            List.filter
+              (fun pp ->
+                F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
               b
           in
           let b = List.map (fun pp -> HPP.find pp_ips d pp) b in
           let e = create (Egraph.context d) in
-          Context.Queue.push (HPT.find pt_ips d fp) (v.ty,e);
-          let b = e::b in
+          Context.Queue.push (HPT.find pt_ips d fp) (v.ty, e);
+          let b = e :: b in
           b
-        end
-      | App(f,_,tl) ->
-        let ips = List.foldi (fun acc pos p ->
-            (aux F_Pos.{ f; pos } pp_vars p)@acc
-          ) [] tl in
-        let ips = List.map (fun ip -> get_fp d ip fp) ips in
-        let ips = (HPC.find pc_ips d PC.{ parent = fp; child = f })::ips in
-        ips
+      | App (f, _, tl) ->
+          let ips =
+            List.foldi
+              (fun acc pos p -> aux F_Pos.{ f; pos } pp_vars p @ acc)
+              [] tl
+          in
+          let ips = List.map (fun ip -> get_fp d ip fp) ips in
+          let ips = HPC.find pc_ips d PC.{ parent = fp; child = f } :: ips in
+          ips
     in
     let pp_vars = Pattern.get_pps trigger.pat in
     match trigger.pat with
     | Var _ -> ()
-    | App(f,_,tl) ->
-        let ips = List.foldi (fun acc pos p ->
-            (aux F_Pos.{ f; pos } pp_vars p)@acc
-        ) [] tl in
+    | App (f, _, tl) ->
+        let ips =
+          List.foldi
+            (fun acc pos p -> aux F_Pos.{ f; pos } pp_vars p @ acc)
+            [] tl
+        in
         List.iter (fun ip -> add_pattern ip trigger) ips
-
 end
 
 let add_trigger d t =
   Trigger.add_trigger d t;
   InvertedPath.insert_pattern d t
 
-let find_new_event d (info:Info.t)  (info':Info.t) =
+let find_new_event d (info : Info.t) (info' : Info.t) =
   let symmetric f acc a b =
-    if CCEqual.physical a b
-    then f acc a b
-    else f (f acc a b) b a
+    if CCEqual.physical a b then f acc a b else f (f acc a b) b a
   in
   let do_pp pp ip acc =
     let aux acc info1 info2 =
-      match F_Pos.M.find_opt pp.PP.parent1 info1.Info.parents,
-            F_Pos.M.find_opt pp.PP.parent1 info2.Info.parents with
+      match
+        ( F_Pos.M.find_opt pp.PP.parent1 info1.Info.parents,
+          F_Pos.M.find_opt pp.PP.parent1 info2.Info.parents )
+      with
       | Some parents, Some _ ->
-        Node.S.fold_left (fun acc n -> InvertedPath.walk d acc n ip) acc parents
+          Node.S.fold_left
+            (fun acc n -> InvertedPath.walk d acc n ip)
+            acc parents
       | _ -> acc
     in
     symmetric aux acc info info'
   in
   let do_pc pc ip acc =
     let aux acc info1 info2 =
-      match F_Pos.M.find_opt pc.PC.parent info1.Info.parents,
-            F.M.find_opt     pc.PC.child  info2.Info.apps with
+      match
+        ( F_Pos.M.find_opt pc.PC.parent info1.Info.parents,
+          F.M.find_opt pc.PC.child info2.Info.apps )
+      with
       | Some parents, Some _ ->
-        Node.S.fold_left (fun acc n -> InvertedPath.walk d acc n ip) acc parents
+          Node.S.fold_left
+            (fun acc n -> InvertedPath.walk d acc n ip)
+            acc parents
       | _ -> acc
     in
     symmetric aux acc info info'
@@ -426,14 +457,21 @@ let find_new_event d (info:Info.t)  (info':Info.t) =
     let aux acc info1 info2 =
       match F_Pos.M.find_opt f_pos info1.Info.parents with
       | Some parents ->
-        Context.Queue.fold (fun acc (ty,ip) ->
-            if Ground.Ty.S.exists (fun gty ->
-                match Pattern.match_ty Expr.Ty.Var.M.empty gty ty with
-                | Error _ -> false
-                | Ok _ -> true) info2.Info.tys
-            then
-              Node.S.fold_left (fun acc n -> InvertedPath.walk d acc n ip) acc parents
-            else acc) acc q
+          Context.Queue.fold
+            (fun acc (ty, ip) ->
+              if
+                Ground.Ty.S.exists
+                  (fun gty ->
+                    match Pattern.match_ty Expr.Ty.Var.M.empty gty ty with
+                    | Error _ -> false
+                    | Ok _ -> true)
+                  info2.Info.tys
+              then
+                Node.S.fold_left
+                  (fun acc n -> InvertedPath.walk d acc n ip)
+                  acc parents
+              else acc)
+            acc q
       | None -> acc
     in
     symmetric aux acc info info'
@@ -447,50 +485,55 @@ let find_new_event d (info:Info.t)  (info':Info.t) =
 let merge d n =
   match Datastructure.HNode.find_opt Info.env d n with
   | None -> ()
-  | Some info ->
-    let n' = Egraph.find d n in
-    match Datastructure.HNode.find_opt Info.env d n' with
-    | None ->
-      Datastructure.HNode.set Info.env d n' info
-    | Some info' ->
-      let info'' = Info.merge info info' in
-      Datastructure.HNode.set Info.env d n' info'';
-      find_new_event d info info'
-
-let skolemize d (e:Ground.ClosedQuantifier.t) =
+  | Some info -> (
+      let n' = Egraph.find d n in
+      match Datastructure.HNode.find_opt Info.env d n' with
+      | None -> Datastructure.HNode.set Info.env d n' info
+      | Some info' ->
+          let info'' = Info.merge info info' in
+          Datastructure.HNode.set Info.env d n' info'';
+          find_new_event d info info' )
+
+let skolemize d (e : Ground.ClosedQuantifier.t) =
   if not (Base.List.is_empty e.ty_vars) then
     invalid_arg "False type quantification";
   let subst_term =
-    List.map (fun v ->
+    List.map
+      (fun v ->
         let id = Expr.Term.Const.mk v.Expr.name [] [] v.ty in
         let t = Expr.Term.apply id [] [] in
-        (v,Ground.convert t))
+        (v, Ground.convert t))
       e.term_vars
   in
   let n =
-    Ground.convert ~subst:{Ground.Subst.ty = Expr.Ty.Var.M.empty;
-                           term = Expr.Term.Var.M.of_list subst_term } e.body in
+    Ground.convert
+      ~subst:
+        {
+          Ground.Subst.ty = Expr.Ty.Var.M.empty;
+          term = Expr.Term.Var.M.of_list subst_term;
+        }
+      e.body
+  in
   Egraph.register d n;
   n
 
-let init,attach =
-  Demon.Fast.register_get_value_daemon
-    ~name:"Quantifier.get_value"
+let init, attach =
+  Demon.Fast.register_get_value_daemon ~name:"Quantifier.get_value"
     (module Boolean.BoolValue)
     (fun d n b th ->
-       match Ground.ThClosedQuantifier.sem th, b with
-       | ({ binder = Exists; _ } as e), true | ({ binder = Forall; _ } as e), false ->
-         Egraph.merge d (skolemize d e) n
-       | { binder = Exists; _ }, false | { binder = Forall; _ }, true ->
-         let triggers = Trigger.compute_triggers th in
-         Debug.dprintf4 debug "[Quant] For %a adds %a"
-           Ground.ThClosedQuantifier.pp th
-           Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp)) triggers;
-         List.iter (add_trigger d) triggers
-    )
-
-let quantifier_registered d th =
-  attach d (Ground.ThClosedQuantifier.node th) th
+      match (Ground.ThClosedQuantifier.sem th, b) with
+      | ({ binder = Exists; _ } as e), true
+      | ({ binder = Forall; _ } as e), false ->
+          Egraph.merge d (skolemize d e) n
+      | { binder = Exists; _ }, false | { binder = Forall; _ }, true ->
+          let triggers = Trigger.compute_triggers th in
+          Debug.dprintf4 debug "[Quant] For %a adds %a"
+            Ground.ThClosedQuantifier.pp th
+            Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
+            triggers;
+          List.iter (add_trigger d) triggers)
+
+let quantifier_registered d th = attach d (Ground.ThClosedQuantifier.node th) th
 
 let add_info_on_ground_terms d thg =
   let res = Ground.node thg in
@@ -499,38 +542,36 @@ let add_info_on_ground_terms d thg =
     let n = Egraph.find_def d n in
     match Datastructure.HNode.find_opt Info.env d n with
     | None ->
-      Datastructure.HNode.set Info.env d n info;
-      find_new_event d info info
+        Datastructure.HNode.set Info.env d n info;
+        find_new_event d info info
     | Some info' ->
-      Datastructure.HNode.set Info.env d n (Info.merge info info');
-      find_new_event d info info;
-      find_new_event d info info'
+        Datastructure.HNode.set Info.env d n (Info.merge info info');
+        find_new_event d info info;
+        find_new_event d info info'
   in
   let add_pc pos n =
-    merge_info n { Info.empty with parents =
-                                     F_Pos.M.singleton { f = g.app; pos }
-                                       (Node.S.singleton res)
-                 }
+    merge_info n
+      {
+        Info.empty with
+        parents = F_Pos.M.singleton { f = g.app; pos } (Node.S.singleton res);
+      }
   in
   List.iteri add_pc g.args;
-  merge_info res { Info.empty with
-                   apps = F.M.singleton g.app (Ground.S.singleton thg);
-                   tys = Ground.Ty.S.singleton g.ty;
-                 };
-  (** Try pattern from the start *)
+  merge_info res
+    {
+      Info.empty with
+      apps = F.M.singleton g.app (Ground.S.singleton thg);
+      tys = Ground.Ty.S.singleton g.ty;
+    };
+  (* Try pattern from the start *)
   let trgs = Trigger.EnvApps.find Trigger.env_apps d g.app in
   Context.Queue.iter (fun trg -> Trigger.match_ d trg res) trgs
 
 let init d =
-  Demon.Fast.register_change_repr_daemon
-    ~name:"Quantifier.merge"
-    merge
-    d;
-  Demon.Fast.register_init_daemon
-    ~name:"Quantifier.new_quantifier"
+  Demon.Fast.register_change_repr_daemon ~name:"Quantifier.merge" merge d;
+  Demon.Fast.register_init_daemon ~name:"Quantifier.new_quantifier"
     (module Ground.ThClosedQuantifier)
-    quantifier_registered
-    d;
+    quantifier_registered d;
   Ground.register_converter d add_info_on_ground_terms;
   init d
 
diff --git a/src_colibri2/theories/quantifier/quantifier.mli b/src_colibri2/theories/quantifier/quantifier.mli
index d8be888cc36ed8675a495c4a6d0be604b343f714..091896da139eb27dbd21aa95722d14114421c306 100644
--- a/src_colibri2/theories/quantifier/quantifier.mli
+++ b/src_colibri2/theories/quantifier/quantifier.mli
@@ -1 +1 @@
-val init: Egraph.t -> unit
+val init : Egraph.t -> unit
diff --git a/src_common/dune b/src_common/dune
index cc74e305ce69649d66e7deac6a25205c6b200175..52f3ee552553fc0693f33b489c21726bf90d53b4 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -2,56 +2,65 @@
  (public_name colibrics.lib)
  (name colibrics_lib)
  (libraries zarith)
- (flags -w -27)
-)
+ (flags -w -27))
 
 (rule
  (targets q__Q.ml)
  (deps q.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . q.Q))
- (mode promote)
-)
-
+ (action
+  (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . q.Q))
+ (mode promote))
 
 (rule
  (targets modulo__Divisible.ml)
  (deps q.mlw modulo.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Divisible))
- (mode promote)
-)
+ (action
+  (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
+    modulo.Divisible))
+ (mode promote))
 
 (rule
  (targets interval__Convexe.ml interval__Bound.ml)
  (deps q.mlw interval.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . interval.Convexe interval.Bound))
- (mode promote)
-)
-
+ (action
+  (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
+    interval.Convexe interval.Bound))
+ (mode promote))
 
 (rule
  (targets interval_with_divider__T.ml)
  (deps q.mlw modulo.mlw interval.mlw interval_with_divider.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . interval_with_divider.T))
- (mode promote)
-)
+ (action
+  (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
+    interval_with_divider.T))
+ (mode promote))
 
 (rule
  (alias runproof)
- (deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q))
-)
+ (deps
+  (source_tree q)
+  q.mlw)
+ (action
+  (run why3 replay -L . q)))
 
 (rule
  (alias runproof)
- (deps (source_tree modulo) modulo.mlw q.mlw)
- (action (run why3 replay -L . modulo))
-)
+ (deps
+  (source_tree modulo)
+  modulo.mlw
+  q.mlw)
+ (action
+  (run why3 replay -L . modulo)))
 
 (rule
  (alias runproof)
- (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
- (action (run why3 replay -L . interval))
-)
+ (deps
+  (source_tree modulo)
+  interval.mlw
+  modulo.mlw
+  q.mlw)
+ (action
+  (run why3 replay -L . interval)))
 
 ; (rule
 ;  (alias ide:q)
@@ -73,18 +82,27 @@
 
 (rule
  (alias runsmokedetector)
- (deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q --smoke-detector deep))
-)
+ (deps
+  (source_tree q)
+  q.mlw)
+ (action
+  (run why3 replay -L . q --smoke-detector deep)))
 
 (rule
  (alias runsmokedetector)
- (deps (source_tree modulo) modulo.mlw q.mlw)
- (action (run why3 replay -L . modulo --smoke-detector deep))
-)
+ (deps
+  (source_tree modulo)
+  modulo.mlw
+  q.mlw)
+ (action
+  (run why3 replay -L . modulo --smoke-detector deep)))
 
 (rule
  (alias runsmokedetector)
- (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
- (action (run why3 replay -L . interval --smoke-detector deep))
-)
+ (deps
+  (source_tree modulo)
+  interval.mlw
+  modulo.mlw
+  q.mlw)
+ (action
+  (run why3 replay -L . interval --smoke-detector deep)))
diff --git a/tests/dune b/tests/dune
index 819e750b0f225a2134935eed4f1dabab6f25ef81..3fbfcae90215c32bbc964f9dfbcac62982c1fe60 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,2 +1,3 @@
 (cram
-    (deps (package colibrics)))
+ (deps
+  (package colibrics)))