diff --git a/opam b/opam
index b7d43c2..981cfaa 100644
--- a/opam
+++ b/opam
@@ -42,12 +42,13 @@ depends: [
   "qcheck"      { with-test & >= "0.8" }
   "dolmen"      { >= "0.4" & < "0.5" }
   "msat"        { >= "0.7" & < "0.8" }
-  "containers"  { >= "2.0" & < "3.0" }
-  "cmdliner"    { >= "0.9.8" }
+  "containers"  { >= "3.6" }
+  "containers-data"  { }
+  "cmdliner"    { >= "0.9.8" & < "2.0.0" }
   "zarith"
   "ocamlgraph"
   "gen"
-  "mtime"
+  "mtime"       { < "2" }
   "iter"        { >= "0.5" }
   "spelll"      { >= "0.3" }
   "uucp"
diff --git a/src/_tags b/src/_tags
index bde4544..6ffebcf 100644
--- a/src/_tags
+++ b/src/_tags
@@ -37,7 +37,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 # Package dependencies
 <**/*>: package(unix), package(zarith), package(msat),      \
         package(cmdliner), package(ocamlgraph),             \
-        package(containers), package(containers.data),      \
+        package(containers), package(containers-data),      \
         package(dolmen), package(iter), package(gen),       \
         package(mtime), package(mtime.clock.os),            \
         package(spelll), package(uucp), package(uutf)
diff --git a/src/algos/rewrite.ml b/src/algos/rewrite.ml
index 047c5a6..5589fa1 100644
--- a/src/algos/rewrite.ml
+++ b/src/algos/rewrite.ml
@@ -234,7 +234,7 @@ module Normalize = struct
   let find_term_match rules t =
     let aux pos t' =
       let aux (rule, m, res) = (rule, m, res, pos) in
-      CCOpt.map aux (match_term_head t' rules)
+      CCOption.map aux (match_term_head t' rules)
     in
     Position.Term.find_map aux t
 
diff --git a/src/algos/superposition.ml b/src/algos/superposition.ml
index 3af7ed8..0ab3fa7 100644
--- a/src/algos/superposition.ml
+++ b/src/algos/superposition.ml
@@ -221,7 +221,7 @@ let compare c c' =
     CCOrd.(Expr.Term.compare a a'
            <?> (Expr.Term.compare, b, b')
            <?> (C.compare, c.map, c'.map))
-  | x, y -> Pervasives.compare (_discr x) (_discr y)
+  | x, y -> Stdlib.compare (_discr x) (_discr y)
 
 (* Printing of clauses *)
 let rec pp_id fmt c =
@@ -331,7 +331,7 @@ let map_rewrites m l =
   in
   List.map (fun (f, m') -> (f, apply m m')) l
 
-let rec compute_rewrites = function
+let compute_rewrites = function
   | Hyp (f, m) ->
     if Mapping.is_empty m then [] else
       begin match f with
@@ -963,7 +963,7 @@ let supp_lit c p_set acc =
 let rewrite p active inactive =
   if ((is_eq inactive.clause && p.rules.rp) ||
       (not @@ is_eq inactive.clause && p.rules.rn)) then
-    CCOpt.map (fun x -> p, x) @@ do_rewrite active inactive
+    CCOption.map (fun x -> p, x) @@ do_rewrite active inactive
   else
     None
 
@@ -1141,7 +1141,7 @@ and discount_loop ~merge p_set =
       Util.debug ~section:p_set.section "@{<yellow>Adding clause@} : %a" pp c;
       if c.lit = Empty then begin
         (* Call the callback *)
-        CCOpt.iter (fun f ->
+        CCOption.iter (fun f ->
             Util.debug ~section:p_set.section
               "@{<magenta>Found empty clause reached@}, %d clauses in state" (S.cardinal p_set.clauses);
             f (Lazy.force c.rewrites) (C.elements c.map)) p_set.callback;
@@ -1202,7 +1202,7 @@ let add_neq t ?f a b =
 
 let debug t =
   Util.debug ~section:t.section "@{<White>Precedence@}: @[<hov>%a@]" pp_precedence t;
-  let l = List.sort (fun c c' -> Pervasives.compare c.id c'.id) @@ S.elements t.clauses in
+  let l = List.sort (fun c c' -> Stdlib.compare c.id c'.id) @@ S.elements t.clauses in
   List.iter (fun c -> Util.debug ~section:t.section " |%@ %a" pp c) l
 
 let solve t =
diff --git a/src/algos/synth.ml b/src/algos/synth.ml
index 093cca0..df4d0b4 100644
--- a/src/algos/synth.ml
+++ b/src/algos/synth.ml
@@ -126,10 +126,10 @@ let term_try ty h f =
   Util.debug ~section "Trying: %a" Expr.Print.const_ty f;
   match Match.ty Mapping.empty Expr.(f.id_type.fun_ret) ty with
   | exception Match.Impossible_ty _ ->
-    Util.debug ~section "  \- unif failed";
+    Util.debug ~section "  \\- unif failed";
     None
   | m ->
-    Util.debug ~section "  \- unif found !";
+    Util.debug ~section "  \\- unif found !";
     (* TODO: allow variables in types of terms to synthetize ? *)
     let m' = List.fold_left (fun acc v ->
         if Mapping.Var.mem_ty acc v then acc
@@ -163,10 +163,10 @@ let term_aux h ty =
   (* Since type metas are replaced by Expr.Ty.base, this is sound *)
   (* Interesting case *)
   | { Expr.ty = Expr.TyApp (f, _) } as ty ->
-    let l = CCFun.(
+    let l =
         iter_on_head f
         |> Iter.filter_map (term_try ty h)
-        |> Iter.to_list) in
+        |> Iter.to_list in
     collapse ty l
 
 let rec perform h task =
diff --git a/src/base/builtin.ml b/src/base/builtin.ml
index 4b1e1c5..e1aa28e 100644
--- a/src/base/builtin.ml
+++ b/src/base/builtin.ml
@@ -415,7 +415,7 @@ module Arith = struct
     | r -> fold_apply s r
 
   let apply f l =
-    match CCOpt.sequence_l (List.map classify l) with
+    match CCOption.sequence_l (List.map classify l) with
     | None -> None
     | Some l' ->
       let t = List.fold_left max_type Int l' in
diff --git a/src/base/expr.ml b/src/base/expr.ml
index 638002b..9c3b7c2 100644
--- a/src/base/expr.ml
+++ b/src/base/expr.ml
@@ -415,7 +415,7 @@ module Subst = struct
       Format.fprintf fmt "@[<hov 2>%a ↦@ %a@]" print_key key print_value value
     in
     Format.fprintf fmt "@[<hv>%a@]"
-      CCFormat.(seq ~sep:(return ";@ ") aux) (Mi.values map)
+      CCFormat.(iter ~sep:(return ";@ ") aux) (Mi.values map)
 
   let debug print_key print_value fmt map =
     let aux fmt ((i, j), (key, value)) =
@@ -519,11 +519,11 @@ module Id = struct
     CCVector.push value_vec None;
     { index; id_name; id_type; id_tags; builtin }
 
-  let ttype ?builtin ?tags name = mk_new ?builtin ?tags:(CCOpt.map ref tags) name Type
-  let ty ?builtin ?tags name ty = mk_new ?builtin ?tags:(CCOpt.map ref tags) name ty
+  let ttype ?builtin ?tags name = mk_new ?builtin ?tags:(CCOption.map ref tags) name Type
+  let ty ?builtin ?tags name ty = mk_new ?builtin ?tags:(CCOption.map ref tags) name ty
 
   let const ?builtin ?tags name fun_vars fun_args fun_ret =
-    mk_new ?builtin ?tags:(CCOpt.map ref tags) name { fun_vars; fun_args; fun_ret; }
+    mk_new ?builtin ?tags:(CCOption.map ref tags) name { fun_vars; fun_args; fun_ret; }
 
   let ty_fun ?builtin ?tags name n =
     const ?builtin ?tags name [] (CCList.replicate n Type) Type
@@ -674,7 +674,7 @@ module Meta = struct
   let hash m = CCHash.(combine2 m.meta_id.index (int m.meta_index))
 
   let compare m1 m2 =
-    CCOrd.(compare m1.meta_index m2.meta_index
+    CCOrd.(poly m1.meta_index m2.meta_index
            <?> (Id.compare, m1.meta_id, m2.meta_id))
 
   let equal m1 m2 = compare m1 m2 = 0
@@ -809,14 +809,14 @@ module Ty = struct
 
   let rec compare u v =
     let hu = hash u and hv = hash v in
-    if hu <> hv then Pervasives.compare hu hv
+    if hu <> hv then Stdlib.compare hu hv
     else match u.ty, v.ty with
       | TyVar v1, TyVar v2 -> Id.compare v1 v2
       | TyMeta m1, TyMeta m2 -> Meta.compare m1 m2
       | TyApp (f1, args1), TyApp (f2, args2) ->
         CCOrd.Infix.(Id.compare f1 f2
                      <?> (CCOrd.list compare, args1, args2))
-      | _, _ -> Pervasives.compare (discr u) (discr v)
+      | _, _ -> Stdlib.compare (discr u) (discr v)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -932,7 +932,7 @@ module Term = struct
 
   let rec compare u v =
     let hu = hash u and hv = hash v in
-    if hu <> hv then Pervasives.compare hu hv
+    if hu <> hv then Stdlib.compare hu hv
     else match u.term, v.term with
       | Var v1, Var v2 -> Id.compare v1 v2
       | Meta m1, Meta m2 -> Meta.compare m1 m2
@@ -940,7 +940,7 @@ module Term = struct
         CCOrd.Infix.(Id.compare f1 f2
                      <?> (CCOrd.list Ty.compare, tys1, tys2)
                      <?> (CCOrd.list compare, args1, args2))
-      | _, _ -> Pervasives.compare (discr u) (discr v)
+      | _, _ -> Stdlib.compare (discr u) (discr v)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -1101,7 +1101,7 @@ module Formula = struct
 
   let rec compare f g =
     let hf = hash f and hg = hash g in
-    if hf <> hg then Pervasives.compare hf hg
+    if hf <> hg then Stdlib.compare hf hg
     else match f.formula, g.formula with
       | True, True | False, False -> 0
       | Equal (u1, v1), Equal(u2, v2) ->
@@ -1118,7 +1118,7 @@ module Formula = struct
         CCOrd.Infix.(CCOrd.list Id.compare tys1 tys2
                      <?> (CCOrd.list Id.compare, ts1, ts2)
                      <?> (compare, h1, h2))
-      | _, _ -> Pervasives.compare (discr f) (discr g)
+      | _, _ -> Stdlib.compare (discr f) (discr g)
 
   let equal u v =
     u == v || (hash u = hash v && compare u v = 0)
@@ -1181,10 +1181,10 @@ module Formula = struct
     | True -> f_false
     | False -> f_true
     | Not f' ->
-      let f_status = CCOpt.get_or ~default:f.f_status status in
+      let f_status = CCOption.get_or ~default:f.f_status status in
       { f' with f_status; }
     | _ ->
-      let status = CCOpt.get_or ~default:f.f_status status in
+      let status = CCOption.get_or ~default:f.f_status status in
       mk_formula ~status (Not f)
 
   let check s = function
@@ -1196,7 +1196,7 @@ module Formula = struct
     let rec aux (o, acc) = function
       | [] -> o, acc
       | ({ formula = And l' } as f) :: r ->
-        let t = CCOpt.get_exn @@ get_tag f f_order in
+        let t = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
         aux (t :: o, List.rev_append l' acc) r
       | a :: r ->
         aux (F a :: o, a :: acc) r
@@ -1213,7 +1213,7 @@ module Formula = struct
     let rec aux (o, acc) = function
       | [] -> o, acc
       | ({ formula = Or l' } as f) :: r ->
-        let t = CCOpt.get_exn @@ get_tag f f_order in
+        let t = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
         aux (t :: o, List.rev_append l' acc) r
       | a :: r ->
         aux (F a :: o, a :: acc) r
@@ -1311,12 +1311,12 @@ module Formula = struct
       if p == new_p then f
       else neg ~status:f.f_status new_p
     | And _ ->
-      let o = CCOpt.get_exn @@ get_tag f f_order in
+      let o = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
       let o'= Order.map (subst_aux ~fix ty_vmap ty_mmap t_vmap t_mmap f_vmap f_mmap) o in
       if Order.for_all2 (==) o o' then f
       else Order.build ~status:f.f_status f_and o'
     | Or l ->
-      let o = CCOpt.get_exn @@ get_tag f f_order in
+      let o = CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag f f_order in
       let o'= Order.map (subst_aux ~fix ty_vmap ty_mmap t_vmap t_mmap f_vmap f_mmap) o in
       if Order.for_all2 (==) o o' then f
       else Order.build ~status:f.f_status f_or o'
diff --git a/src/base/position.ml b/src/base/position.ml
index 9484202..58324be 100644
--- a/src/base/position.ml
+++ b/src/base/position.ml
@@ -31,7 +31,7 @@ let follow t i = concat t (path [i])
 
 (* Comparison, equality, printing. *)
 let equal = (=)
-let compare = Pervasives.compare
+let compare = Stdlib.compare
 
 let rec print fmt = function
   | Here -> Format.fprintf fmt "."
@@ -73,15 +73,15 @@ module Proof = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (0, p'), { Term.term = Term.App (f, arg) } ->
-      CCOpt.map (fun x -> Term.app x arg) (substitute p' ~by:u f)
+      CCOption.map (fun x -> Term.app x arg) (substitute p' ~by:u f)
     | Arg (1, p'), { Term.term = Term.App (f, arg) } ->
-      CCOpt.map (fun x -> Term.app f x) (substitute p' ~by:u arg)
+      CCOption.map (fun x -> Term.app f x) (substitute p' ~by:u arg)
     | Arg (0, p'), { Term.term = Term.Let (v, e, body) } ->
-      CCOpt.map (fun x -> Term.letin v x body) (substitute p' ~by:u e)
+      CCOption.map (fun x -> Term.letin v x body) (substitute p' ~by:u e)
     | Arg (1, p'), { Term.term = Term.Let (v, e, body) } ->
-      CCOpt.map (fun x -> Term.letin v e x) (substitute p' ~by:u body)
+      CCOption.map (fun x -> Term.letin v e x) (substitute p' ~by:u body)
     | Arg (0, p'), { Term.term = Term.Binder (b, v, body) } ->
-      CCOpt.map (fun x -> Term.bind b v x) (substitute p' ~by:u body)
+      CCOption.map (fun x -> Term.bind b v x) (substitute p' ~by:u body)
     | Arg _, _ -> None
 
   let rec find_aux cur_pos u t =
@@ -90,11 +90,11 @@ module Proof = struct
       | { Term.term = Term.Type }
       | { Term.term = Term.Id _ } -> None
       | { Term.term = Term.App (f, arg) } ->
-        CCOpt.or_lazy
+        CCOption.or_lazy
           (find_aux (fun p -> cur_pos (Arg (0, p))) u f)
           ~else_:(fun () -> find_aux (fun p -> cur_pos (Arg (1, p))) u arg)
       | { Term.term = Term.Let (_, e, body) } ->
-        CCOpt.or_lazy
+        CCOption.or_lazy
           (find_aux (fun p -> cur_pos (Arg (0, p))) u e)
           ~else_:(fun () -> find_aux (fun p -> cur_pos (Arg (1, p))) u body)
       | { Term.term = Term.Binder (_, _, body) } ->
@@ -126,7 +126,7 @@ module Ty = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (k, p'), { Expr.ty = Expr.TyApp(f, l) } ->
-      CCOpt.map (Expr.Ty.apply ~status:t.Expr.ty_status f) @@ CCOpt.sequence_l
+      CCOption.map (Expr.Ty.apply ~status:t.Expr.ty_status f) @@ CCOption.sequence_l
         (List.mapi (fun i v -> if i = k then substitute p' ~by:u v else Some v) l)
     | _ -> None
 
@@ -175,7 +175,7 @@ module Term = struct
     match p, t with
     | Here, _ -> Some u
     | Arg (k, p'), { Expr.term = Expr.App(f, tys, l) } ->
-      CCOpt.map (Expr.Term.apply ~status:t.Expr.t_status f tys) @@ CCOpt.sequence_l
+      CCOption.map (Expr.Term.apply ~status:t.Expr.t_status f tys) @@ CCOption.sequence_l
         (List.mapi (fun i v -> if i = k then substitute p' ~by:u v else Some v) l)
     | _ -> None
 
diff --git a/src/base/tag.ml b/src/base/tag.ml
index 68c2b56..94b0991 100644
--- a/src/base/tag.ml
+++ b/src/base/tag.ml
@@ -10,7 +10,7 @@
 module M = CCMixmap.Make(struct
     type t = int
     let compare (a: int) (b: int) =
-      Pervasives.compare a b
+      Stdlib.compare a b
   end)
 
 type map = M.t
diff --git a/src/base/type.ml b/src/base/type.ml
index 1d5b369..726c9cf 100644
--- a/src/base/type.ml
+++ b/src/base/type.ml
@@ -13,7 +13,7 @@ module Id = Dolmen.Id
 
 let get_loc =
   let default_loc = Dolmen.ParseLocation.mk "<?>" 0 0 0 0 in
-  (fun t -> CCOpt.get_or ~default:default_loc t.Ast.loc)
+  (fun t -> CCOption.get_or ~default:default_loc t.Ast.loc)
 
 module E = Map.Make(Expr.Id.Ttype)
 module F = Map.Make(Expr.Id.Ty)
@@ -1028,7 +1028,7 @@ let new_decl env t ?attr id =
     Id.print id Ast.print t;
   let aux acc (Any (tag, v)) = Tag.add acc tag v in
   let tags =
-    CCOpt.map (fun a ->
+    CCOption.map (fun a ->
         Util.debug ~section "Typing attribute:@ @[<hov>%a@]" Ast.print a;
         let l = parse_attr_and env a in
         List.fold_left aux Tag.empty l) attr
diff --git a/src/core/dispatcher.ml b/src/core/dispatcher.ml
index e458012..c62814a 100644
--- a/src/core/dispatcher.ml
+++ b/src/core/dispatcher.ml
@@ -163,11 +163,11 @@ let mk_ext
   Stats.attach section plugin_stats_group;
   {
     section;
-    set_handler = CCOpt.map (profile section) set_handler;
-    set_watcher = CCOpt.map (profile section) set_watcher;
-    assume = CCOpt.map (profile section) assume;
-    eval_pred = CCOpt.map (profile section) eval_pred;
-    preprocess = CCOpt.map (profile section) preprocess;
+    set_handler = CCOption.map (profile section) set_handler;
+    set_watcher = CCOption.map (profile section) set_watcher;
+    assume = CCOption.map (profile section) assume;
+    eval_pred = CCOption.map (profile section) eval_pred;
+    preprocess = CCOption.map (profile section) preprocess;
     handle = match handle with
       | None -> None
       | Some h ->
@@ -492,9 +492,9 @@ let stack_assign_level () =
 
 (** Call/execute a single job *)
 let call_job j =
-  if not CCOpt.(get_or ~default:true (j.job_formula >>= get_truth)) then
+  if not CCOption.(get_or ~default:true (j.job_formula >>= get_truth)) then
     Util.debug ~section:watch_section "Ignoring job %a because of false formula:@ %a"
-      pp_job j Expr.Formula.print (CCOpt.get_exn j.job_formula)
+      pp_job j Expr.Formula.print (CCOption.get_exn_or "CCOption.get_exn_or" j.job_formula)
   else begin
     Util.debug ~section:watch_section "Calling job %a" pp_job j;
     profile j.job_section j.job_callback ()
@@ -535,8 +535,8 @@ let cancel_jobs lvl =
       new_size := !new_size + 1
     end
   done;
-  let () = CCVector.shrink job_trail !new_size in
-  let () = CCVector.shrink job_level lvl in
+  let () = CCVector.truncate job_trail !new_size in
+  let () = CCVector.truncate job_level lvl in
   job_idx := j_lvl
 
 
diff --git a/src/core/ext_arith.ml b/src/core/ext_arith.ml
index e5e27fe..6018598 100644
--- a/src/core/ext_arith.ml
+++ b/src/core/ext_arith.ml
@@ -35,11 +35,11 @@ let evaluate_aux t =
   Arith.M.fold (fun e c acc ->
       match Dispatcher.get_assign e with
       | { Expr.term = Expr.App ({ Expr.builtin = B.Val v}, [], []) } ->
-        CCOpt.map (fun acc -> Q.(acc + c * val_to_q v)) acc
+        CCOption.map (fun acc -> Q.(acc + c * val_to_q v)) acc
       | _ -> None
     ) t.Arith.Lit.sum (Some (val_to_q t.Arith.Lit.const))
 
-let evaluate t = CCOpt.map evaluate_aux @@ Arith.Lit.parse_num t
+let evaluate t = CCOption.map evaluate_aux @@ Arith.Lit.parse_num t
 *)
 (* Incomplete extension *)
 (* ************************************************************************ *)
diff --git a/src/core/ext_prop.ml b/src/core/ext_prop.ml
index ea61451..e59ed68 100644
--- a/src/core/ext_prop.ml
+++ b/src/core/ext_prop.ml
@@ -32,7 +32,7 @@ let rec sat_eval = function
         None
     end
   | { Expr.formula = Expr.Not f } ->
-    CCOpt.map (fun (b, l) -> (not b, l)) (sat_eval f)
+    CCOption.map (fun (b, l) -> (not b, l)) (sat_eval f)
   | _ -> None
 
 (* Setup watchers *)
diff --git a/src/core/ext_rewrite.ml b/src/core/ext_rewrite.ml
index adb9e4f..108930e 100644
--- a/src/core/ext_rewrite.ml
+++ b/src/core/ext_rewrite.ml
@@ -329,9 +329,9 @@ let parse_guard = function
 
 let parse_guards = function
   | { Expr.formula = Expr.And l } ->
-    CCOpt.sequence_l (List.map parse_guard l)
+    CCOption.sequence_l (List.map parse_guard l)
   | f ->
-    CCOpt.map (fun x -> [x]) (parse_guard f)
+    CCOption.map (fun x -> [x]) (parse_guard f)
 
 (* Parse manually oriented rules *)
 let rec parse_manual_rule = function
@@ -372,7 +372,7 @@ let rec parse_manual_rule = function
 
   (* Conditional rewriting *)
   | { Expr.formula = Expr.Imply (cond, r) } ->
-    CCOpt.map2 Rewrite.Rule.add_guards (parse_guards cond) (parse_manual_rule r)
+    CCOption.map2 Rewrite.Rule.add_guards (parse_guards cond) (parse_manual_rule r)
 
   (* Not a rewrite rule, :p *)
   | _ -> None
@@ -404,7 +404,7 @@ let rec parse_rule_aux = function
 
   (* Conditional rewriting *)
   | { Expr.formula = Expr.Imply (cond, r) } ->
-    CCOpt.map2 Rewrite.Rule.add_guards (parse_guards cond) (parse_rule_aux r)
+    CCOption.map2 Rewrite.Rule.add_guards (parse_guards cond) (parse_rule_aux r)
 
   (* Other formulas are not rewrite rules *)
   | _ -> None
@@ -413,7 +413,7 @@ let rec parse_rule_aux = function
 let parse_rule = function
   (* TODO: check that some variables are actually used in the rule ? *)
   | ({ Expr.formula = Expr.All (_, _, r) } as formula) ->
-    let manual = CCOpt.is_some (Expr.Formula.get_tag formula Builtin.Tag.rwrt) in
+    let manual = CCOption.is_some (Expr.Formula.get_tag formula Builtin.Tag.rwrt) in
     let parse = if manual then parse_manual_rule else parse_rule_aux in
     begin match parse r with
       | None ->
@@ -728,7 +728,7 @@ and proof_term goal r s trigger result pos =
   | Some p ->
     pos
     |> Eq.subst p goal ~by:result_t ~eq:(proof_inst s)
-    |> proof_chain (CCOpt.get_exn @@ Position.Proof.substitute p ~by:result_t goal) r
+    |> proof_chain (CCOption.get_exn_or "CCOption.get_exn_or" @@ Position.Proof.substitute p ~by:result_t goal) r
   | None ->
     raise (Proof.Failure ("Ext_rewrite.proof_chain", pos))
 
@@ -742,21 +742,21 @@ and proof_prop goal r s trigger result pos =
   let result_t = Term.of_formula result in
   Util.debug ~section "@[<v>trigger_t: %a@ result_t: %a@]"
     Term.print trigger_t Term.print result_t;
-  let (left, right) = CCOpt.get_exn @@ Logic.match_equiv goal in
+  let (left, right) = CCOption.get_exn_or "CCOption.get_exn_or" @@ Logic.match_equiv goal in
   begin match Position.Proof.find trigger_t goal with
     | Some p ->
       if Term.Reduced.equal left trigger_t ||
          Term.Reduced.equal right trigger_t then begin
         pos
         |> Logic.equiv_replace trigger_t ~by:result_t ~equiv:(proof_inst s)
-        |> proof_chain (CCOpt.get_exn @@ Position.Proof.substitute p ~by:result_t goal) r
+        |> proof_chain (CCOption.get_exn_or "CCOption.get_exn_or" @@ Position.Proof.substitute p ~by:result_t goal) r
       end else begin
         pos
         |> Logic.equiv_replace
           (Term.app Term.not_term trigger_t)
           ~by:(Term.app Term.not_term result_t)
           ~equiv:(proof_inst_not s)
-        |> proof_chain (CCOpt.get_exn @@ Position.Proof.substitute p ~by:result_t goal) r
+        |> proof_chain (CCOption.get_exn_or "CCOption.get_exn_or" @@ Position.Proof.substitute p ~by:result_t goal) r
       end
     | None ->
       Util.error ~section "@[<hv>Position not found for@ %a@ in@ %a@]"
diff --git a/src/core/ext_skolem.ml b/src/core/ext_skolem.ml
index 7ffee27..4f965de 100644
--- a/src/core/ext_skolem.ml
+++ b/src/core/ext_skolem.ml
@@ -80,10 +80,10 @@ let prelude_tag = Tag.create ()
 
 let prelude_of_deps (tys, ts) =
   Sterm.fold (fun t l ->
-      CCOpt.get_exn (Expr.Term.get_tag t prelude_tag) :: l
+      CCOption.get_exn_or "CCOption.get_exn_or" (Expr.Term.get_tag t prelude_tag) :: l
     ) ts @@
   Sty.fold (fun ty l ->
-      CCOpt.get_exn (Expr.Ty.get_tag ty prelude_tag) :: l
+      CCOption.get_exn_or "CCOption.get_exn_or" (Expr.Ty.get_tag ty prelude_tag) :: l
     ) tys [Quant.epsilon_prelude]
 
 let inst_epsilon get_eps add_eps get_tag tag trap inhabited e t =
@@ -97,7 +97,7 @@ let inst_epsilon get_eps add_eps get_tag tag trap inhabited e t =
         let eps_term = Term.apply Quant.epsilon_term [x.Expr.id_type; inhabited; p] in
         let eps = Term.define (epsilon_name ()) eps_term in
         let eps_t = Term.id eps in
-        let deps = prelude_of_deps @@ CCOpt.get_exn @@ get_tag e dep_tag in
+        let deps = prelude_of_deps @@ CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag e dep_tag in
         let alias = Proof.Prelude.alias ~deps eps (fun _ -> Some eps_term) in
         let () = add_eps e eps_t in
         let () = tag e prelude_tag alias in
@@ -106,7 +106,7 @@ let inst_epsilon get_eps add_eps get_tag tag trap inhabited e t =
     in
     Term.(subst (S.Id.bind S.empty x eps_t)) body
   | _ ->
-    begin match CCOpt.(Logic.match_not t >>= Quant.match_all) with
+    begin match CCOption.(Logic.match_not t >>= Quant.match_all) with
       | Some (x, body) ->
         let body =
           match Logic.match_not body with
@@ -120,7 +120,7 @@ let inst_epsilon get_eps add_eps get_tag tag trap inhabited e t =
             let eps_term = Term.apply Quant.epsilon_term [x.Expr.id_type; inhabited; p] in
             let eps = Term.define (epsilon_name ()) eps_term in
             let eps_t = Term.id eps in
-            let deps = prelude_of_deps @@ CCOpt.get_exn @@ get_tag e dep_tag in
+            let deps = prelude_of_deps @@ CCOption.get_exn_or "CCOption.get_exn_or" @@ get_tag e dep_tag in
             let alias = Proof.Prelude.alias ~deps eps (fun _ -> Some eps_term) in
             let () = add_eps e eps_t in
             let () = tag e prelude_tag alias in
@@ -271,8 +271,8 @@ let coq_proof = function
   | Inst ( { Expr.formula = Expr.Ex _ } as f, tys, ts, res) ->
     (** We want to prove ~ ~ [ exists _, body] -> ~ body -> False,
         note that [body] may be a negation. *)
-    let deps = List.map (fun ty -> CCOpt.get_exn @@ Expr.Ty.get_tag ty prelude_tag) tys @
-               List.map (fun t -> CCOpt.get_exn @@ Expr.Term.get_tag t prelude_tag) ts in
+    let deps = List.map (fun ty -> CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Ty.get_tag ty prelude_tag) tys @
+               List.map (fun t -> CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Term.get_tag t prelude_tag) ts in
     let args = List.map Term.of_ty tys @
                List.map Term.of_term ts in
     let witnesses = List.map (fun _ -> Term.of_ty Synth.ty) tys @
@@ -289,8 +289,8 @@ let coq_proof = function
       Expr.formula = Expr.All _ } } as f, tys, ts, res) ->
     (** We want to prove ~ [ all _, body] -> ~ ~ body -> False (res = ~ body)
                       or ~ [ all _, ~ body] -> ~ body -> False (res = body) *)
-    let deps = List.map (fun ty -> CCOpt.get_exn @@ Expr.Ty.get_tag ty prelude_tag) tys @
-               List.map (fun t -> CCOpt.get_exn @@ Expr.Term.get_tag t prelude_tag) ts in
+    let deps = List.map (fun ty -> CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Ty.get_tag ty prelude_tag) tys @
+               List.map (fun t -> CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Term.get_tag t prelude_tag) ts in
     let args = List.map Term.of_ty tys @
                List.map Term.of_term ts in
     let witnesses = List.map (fun _ -> Term.of_ty Synth.ty) tys @
diff --git a/src/core/inst.ml b/src/core/inst.ml
index 5bd4a91..4c8f3d9 100644
--- a/src/core/inst.ml
+++ b/src/core/inst.ml
@@ -134,13 +134,13 @@ let mk_t_var =
 
 let indexes l l' =
   let aux m = m.Expr.meta_index in
-  CCList.sort_uniq ~cmp:Pervasives.compare (List.map aux l @ List.map aux l')
+  CCList.sort_uniq ~cmp:Stdlib.compare (List.map aux l @ List.map aux l')
 
 let meta_of_indexes l =
-  CCFun.(l
-         |> CCList.map Expr.Meta.of_index
-         |> CCList.split
-         |> CCPair.map CCList.flatten CCList.flatten)
+  l
+  |> CCList.map Expr.Meta.of_index
+  |> CCList.split
+  |> CCPair.map CCList.flatten CCList.flatten
 
 let generalize_aux m =
   Util.debug ~section "Generalizing@ %a" Mapping.print m;
diff --git a/src/debug/section.ml b/src/debug/section.ml
index 3df4305..2230c6d 100644
--- a/src/debug/section.ml
+++ b/src/debug/section.ml
@@ -216,7 +216,7 @@ let enter section =
       active := section :: !active
     | _ ->
       if not (is_parent_active section) then
-        ignore (CCOpt.map prof_exit (curr ()));
+        ignore (CCOption.map prof_exit (curr ()));
       prof_enter section;
       active := section :: !active
   end
diff --git a/src/input/options.ml b/src/input/options.ml
index 8511ea2..b8dadd8 100644
--- a/src/input/options.ml
+++ b/src/input/options.ml
@@ -376,8 +376,8 @@ let log_opts opt =
     (bool_opt "prove" opt.proof.active)
     (bool_opt "translate" opt.translate)
     (bool_opt "profile" opt.profile.enabled)
-    (CCOpt.get_or ~default:"auto" @@
-     CCOpt.map In.string_of_language @@ opt.input.format)
+    (CCOption.get_or ~default:"auto" @@
+     CCOption.map In.string_of_language @@ opt.input.format)
     (output_string opt.output.format);
   Util.log "Input dir : '%s'" opt.input.dir;
   Util.log "Input file : %s" (input_to_string opt.input.file)
@@ -481,7 +481,7 @@ let log_sections () =
   let l = ref [] in
   Section.iter (fun s ->
       if not Section.(equal root s) then l := Section.full_name s :: !l);
-  List.sort Pervasives.compare !l
+  List.sort Stdlib.compare !l
 
 let gc_t =
   let docs = gc_sect in
diff --git a/src/main.ml b/src/main.ml
index bf26dac..b8d2882 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -35,7 +35,7 @@ let () =
       if opt.profile.enabled then begin
         at_exit Section.print_profiling_info;
         Section.set_profile_depth
-          (CCOpt.get_or ~default:0 opt.profile.max_depth);
+          (CCOption.get_or ~default:0 opt.profile.max_depth);
         List.iter Section.profile_section opt.profile.sections
       end;
 
diff --git a/src/middle/pipe.ml b/src/middle/pipe.ml
index 2bbe367..919371b 100644
--- a/src/middle/pipe.ml
+++ b/src/middle/pipe.ml
@@ -208,7 +208,7 @@ let prove_id = stmt_id "prove"
 
 (* TODO, unwind backtrak stack on exceptions ? *)
 let type_wrap ?(goal=false) opt =
-  let l = CCOpt.get_exn Options.(opt.input.format) in
+  let l = CCOption.get_exn_or "CCOption.get_exn_or" Options.(opt.input.format) in
   let status =
     if goal then Expr.Status.goal
     else Expr.Status.hypothesis
@@ -240,7 +240,7 @@ let run_typecheck opt = Options.(opt.typing.typing)
 
 let fv_list l =
   let l' = List.map Dolmen.Term.fv l in
-  CCList.sort_uniq Dolmen.Id.compare (List.flatten l')
+  CCList.sort_uniq ~cmp:Dolmen.Id.compare (List.flatten l')
 
 let typecheck (opt, c) : typechecked stmt =
   Util.enter_prof Type.section;
diff --git a/src/output/std.ml b/src/output/std.ml
index 640c0c3..2f94fee 100644
--- a/src/output/std.ml
+++ b/src/output/std.ml
@@ -17,7 +17,7 @@ let prelude_space opt =
 let default_loc opt = Dolmen.ParseLocation.mk
     (Options.input_to_string Options.(opt.input.file)) 0 0 0 0
 
-let get_loc opt loc = CCOpt.get_or ~default:(default_loc opt) loc
+let get_loc opt loc = CCOption.get_or ~default:(default_loc opt) loc
 
 (* Output functions *)
 (* ************************************************************************ *)
@@ -60,7 +60,7 @@ let print_exn opt fmt = function
   | Options.Stmt_not_implemented s ->
     let default_loc = Dolmen.ParseLocation.mk
         (Options.input_to_string Options.(opt.input.file)) 0 0 0 0 in
-    let loc = CCOpt.get_or ~default:default_loc s.Dolmen.Statement.loc in
+    let loc = CCOption.get_or ~default:default_loc s.Dolmen.Statement.loc in
     Format.fprintf Format.std_formatter
       "%a: the following statement is not yet treated:@\n%a@."
       Dolmen.ParseLocation.fmt loc Dolmen.Statement.print s
diff --git a/src/proof/coq.ml b/src/proof/coq.ml
index b9cbf87..6d44a59 100644
--- a/src/proof/coq.ml
+++ b/src/proof/coq.ml
@@ -73,7 +73,7 @@ module Print = struct
       if Term.is_coq_implicit v then elim_implicits body tl
       else if Term.is_coq_inferred v then None :: elim_implicits body tl
       else Some hd :: elim_implicits body tl
-    | _ -> List.map CCOpt.return args
+    | _ -> List.map CCOption.return args
 
   let rec term_aux ~simplify ~fragile fmt t =
     let t = if simplify then Term.contract t else t in
diff --git a/src/proof/eq.ml b/src/proof/eq.ml
index 8b35968..a5d9fae 100644
--- a/src/proof/eq.ml
+++ b/src/proof/eq.ml
@@ -3,8 +3,8 @@
 let section = Section.make ~parent:Proof.section "eq"
 
 let tag ?dk ?coq id =
-  CCOpt.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
-  CCOpt.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
+  CCOption.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
+  CCOption.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
   ()
 
 (* Useful constants *)
diff --git a/src/proof/logic.ml b/src/proof/logic.ml
index aad4198..26238d2 100644
--- a/src/proof/logic.ml
+++ b/src/proof/logic.ml
@@ -3,8 +3,8 @@
 let section = Section.make ~parent:Proof.section "logic"
 
 let tag ?dk ?coq id =
-  CCOpt.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
-  CCOpt.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
+  CCOption.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
+  CCOption.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
   ()
 
 (* Logic preludes *)
@@ -468,7 +468,7 @@ let match_equiv_not t =
     end
   | None -> None
 
-let match_not_not t = CCOpt.(match_not t >>= match_not)
+let match_not_not t = CCOption.(match_not t >>= match_not)
 
 let shortcut_not_not t =
   match match_not_not t with Some t' -> t' | None -> t
diff --git a/src/proof/proof.ml b/src/proof/proof.ml
index 3d474df..c6f327a 100644
--- a/src/proof/proof.ml
+++ b/src/proof/proof.ml
@@ -247,7 +247,7 @@ module Prelude = struct
       match t, t' with
       | Require v, Require v' -> Expr.Id.compare v v'
       | Alias (v, e), Alias (v', e') -> Expr.Id.compare v v'
-      | _ -> Pervasives.compare (_discr t) (_discr t')
+      | _ -> Stdlib.compare (_discr t) (_discr t')
 
     let equal t t' = compare t t' = 0
 
@@ -270,7 +270,7 @@ module Prelude = struct
       Format.fprintf fmt "(* Prelude: Module import *)@\nRequire Import %a.@\n" Coq.Print.id id
     | Alias (id, f) ->
       Util.debug ~section "%a : %a" Expr.Id.print id Term.print id.Expr.id_type;
-      CCOpt.iter (fun t ->
+      CCOption.iter (fun t ->
           Format.fprintf fmt
             "(* @[<hov>Prelude: Alias@] *)@\n@[<hv>pose ( %a :=@ @[<hov>%a@] )@].@\n"
             Coq.Print.id id Coq.Print.fragile t
@@ -280,7 +280,7 @@ module Prelude = struct
     | Require id ->
       Format.fprintf fmt "(* Prelude: Module import *)@\nRequire Import %a.@\n" Coq.Print.id id
     | Alias (id, f) ->
-      CCOpt.iter (fun t ->
+      CCOption.iter (fun t ->
           Format.fprintf fmt
             "(* @[<hov>Prelude: Alias@] *)@\n@[<hv>Definition %a :@ @[<hov>%a@] :=@ @[<hov>%a@]@].@\n"
             Coq.Print.id id Coq.Print.term id.Expr.id_type Coq.Print.fragile t
@@ -291,7 +291,7 @@ module Prelude = struct
       Format.fprintf fmt
         "(; Prelude: Module import (%a) -- not needed in dedukti;)@." Dedukti.Print.id id
     | Alias (id, f) ->
-      CCOpt.iter (fun t ->
+      CCOption.iter (fun t ->
           Format.fprintf fmt
             "(; Prelude: Alias ;)@\n@[<hv 2>def %a :=@ @[<hov>%a@]@].@\n"
             Dedukti.Print.id id Dedukti.Print.fragile t
diff --git a/src/proof/prove.ml b/src/proof/prove.ml
index 1fd3ec8..d31e490 100644
--- a/src/proof/prove.ml
+++ b/src/proof/prove.ml
@@ -36,10 +36,10 @@ let pp_lazy lang s o x pp =
   | Some fmt ->
     begin try
         let p = Lazy.force x in
-        CCOpt.iter (Util.log ~section "Printing proof for %s") lang;
+        CCOption.iter (Util.log ~section "Printing proof for %s") lang;
         Util.enter_prof s;
         Format.fprintf fmt "%a@." pp p;
-        CCOpt.iter (Util.info ~section "Finished printing proof for %s") lang;
+        CCOption.iter (Util.info ~section "Finished printing proof for %s") lang;
         Util.exit_prof s
       with
       | Proof.Open_proof ->
diff --git a/src/proof/quant.ml b/src/proof/quant.ml
index 44d52b9..71d5497 100644
--- a/src/proof/quant.ml
+++ b/src/proof/quant.ml
@@ -3,8 +3,8 @@
 let section = Section.make ~parent:Proof.section "quant"
 
 let tag ?dk ?coq id =
-  CCOpt.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
-  CCOpt.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
+  CCOption.iter (fun s -> Expr.Id.tag id Dedukti.Print.name @@ Pretty.Exact s) dk;
+  CCOption.iter (fun s -> Expr.Id.tag id Coq.Print.name @@ Pretty.Exact s) coq;
   ()
 
 (* Epsilon prelude *)
@@ -129,10 +129,10 @@ let match_ex =
        assert false)
 
 let match_not_ex t =
-  CCOpt.(Logic.match_not t >>= match_ex)
+  CCOption.(Logic.match_not t >>= match_ex)
 
 let match_not_all t =
-  CCOpt.(Logic.match_not t >>= match_all)
+  CCOption.(Logic.match_not t >>= match_all)
 
 (* Instanciation *)
 (* ************************************************************************ *)
diff --git a/src/proof/term.ml b/src/proof/term.ml
index 2f17b6a..6b7620d 100644
--- a/src/proof/term.ml
+++ b/src/proof/term.ml
@@ -77,7 +77,7 @@ let pp fmt t =
 (* ************************************************************************ *)
 
 let hash t = t.hash
-let compare t t' = Pervasives.compare t.index t'.index
+let compare t t' = Stdlib.compare t.index t'.index
 let equal t t' = compare t t' = 0
 
 let ty t = Lazy.force t.ty
@@ -168,8 +168,8 @@ let define s def =
 
 let merge s s' =
   S.merge (fun _ o o' ->
-      let n = CCOpt.get_or ~default:0 o in
-      let m = CCOpt.get_or ~default:0 o' in
+      let n = CCOption.get_or ~default:0 o in
+      let m = CCOption.get_or ~default:0 o' in
       assert (n >= 0 && m >= 0);
       let res = n + m in
       if res = 0 then None else Some res
@@ -732,7 +732,7 @@ let rec uncurry_assoc_right f l =
 let uncurry ?assoc t =
   match uncurry_app t with
   | ({ term = Id f } as f_t), l ->
-    let l = CCOpt.(
+    let l = CCOption.(
         map_or ~default:l (function
             | Pretty.Left -> uncurry_assoc_left f l
             | Pretty.Right -> uncurry_assoc_right f l)
@@ -1047,7 +1047,7 @@ and of_formula_aux ?callback f =
     let y' = of_term ?callback y in
     let ty = ty x' in
     let a, b =
-      match CCOpt.get_exn @@ Expr.Formula.get_tag f Expr.t_order with
+      match CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Formula.get_tag f Expr.t_order with
       | Expr.Same -> x', y'
       | Expr.Inverse -> y', x'
     in
@@ -1061,10 +1061,10 @@ and of_formula_aux ?callback f =
     apply equiv_term [of_formula ?callback p; of_formula ?callback q]
 
   | Expr.Or _ ->
-    let order = CCOpt.get_exn @@ Expr.Formula.get_tag f Expr.f_order in
+    let order = CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Formula.get_tag f Expr.f_order in
     of_tree ?callback or_term order
   | Expr.And l ->
-    let order = CCOpt.get_exn @@ Expr.Formula.get_tag f Expr.f_order in
+    let order = CCOption.get_exn_or "CCOption.get_exn_or" @@ Expr.Formula.get_tag f Expr.f_order in
     of_tree ?callback and_term order
 
   | Expr.All ((tys, ts), _, body) ->
diff --git a/src/proof/unsat_core.ml b/src/proof/unsat_core.ml
index 20029fa..e6f7c5b 100644
--- a/src/proof/unsat_core.ml
+++ b/src/proof/unsat_core.ml
@@ -25,15 +25,15 @@ module S = Set.Make(struct
       match n1.P.step, n2.P.step with
       | P.Lemma l1, P.Lemma l2 ->
         let open CCOrd in
-        map (fun l -> l.D.plugin_name) compare l1 l2
-        <?> (map (fun l -> l.D.proof_name) compare, l1, l2)
+        map (fun l -> l.D.plugin_name) poly l1 l2
+        <?> (map (fun l -> l.D.proof_name) poly, l1, l2)
         <?> (compare_clause, n1.P.conclusion, n2.P.conclusion)
       | P.Hypothesis, P.Hypothesis
       | P.Assumption, P.Assumption
       | P.Duplicate _, P.Duplicate _
       | P.Resolution _, P.Resolution _ ->
         compare_clause n1.P.conclusion n2.P.conclusion
-      | a, b -> Pervasives.compare (discr a) (discr b)
+      | a, b -> Stdlib.compare (discr a) (discr b)
 
   end)
 
diff --git a/src/test/closure_test.ml b/src/test/closure_test.ml
index 1de18e7..4c64c49 100644
--- a/src/test/closure_test.ml
+++ b/src/test/closure_test.ml
@@ -96,8 +96,8 @@ let check_proof l (a, b, chain) =
       Expr.Term.((equal a c && equal b d) ||
                  (equal a d && equal b c))) neq &&
   List.for_all (fun (c, d) -> S.mem d (find t c).eq) (pairify chain) &&
-  CCOpt.map_or ~default:false (Expr.Term.equal a) (CCList.head_opt chain) &&
-  CCOpt.map_or ~default:false (Expr.Term.equal b) (CCList.last_opt chain)
+  CCOption.map_or ~default:false (Expr.Term.equal a) (CCList.head_opt chain) &&
+  CCOption.map_or ~default:false (Expr.Term.equal b) (CCList.last_opt chain)
 
 (* Checking Closure *)
 (* ************************************************************************ *)
diff --git a/src/util/arith.ml b/src/util/arith.ml
index 47a32aa..b0fa5c8 100644
--- a/src/util/arith.ml
+++ b/src/util/arith.ml
@@ -24,16 +24,16 @@ module Mod = struct
           begin match compare d.power d'.power with
             | 0 ->
               if not (Z.equal k k') then None
-              else CCOpt.map (cons (k, d)) (merge r r')
+              else CCOption.map (cons (k, d)) (merge r r')
             | x when x < 0 ->
               if not (Z.equal (Z.erem k' (value d)) k) then None
-              else CCOpt.map (cons (k', d')) (merge r r')
+              else CCOption.map (cons (k', d')) (merge r r')
             | _(* x > 0 *) ->
               if not (Z.equal (Z.erem k (value d')) k') then None
-              else CCOpt.map (cons (k, d)) (merge r r')
+              else CCOption.map (cons (k, d)) (merge r r')
           end
-        | x when x < 0 -> CCOpt.map (cons (k, d)) (merge r l')
-        | _(* x > 0 *) -> CCOpt.map (cons (k', d')) (merge l r')
+        | x when x < 0 -> CCOption.map (cons (k, d)) (merge r l')
+        | _(* x > 0 *) -> CCOption.map (cons (k', d')) (merge l r')
       end
 
   let sum_up l =
@@ -80,16 +80,16 @@ module Lit = struct
   let rec parse_num = function
     | { Expr.term = Expr.App ({ Expr.builtin = A.Val v}, [], []) } -> Some (const v)
     | { Expr.term = Expr.App ({ Expr.builtin = A.Op A.Minus}, [], [e]) } ->
-      CCOpt.map (times (A.Int Z.(- one))) (parse_num e)
+      CCOption.map (times (A.Int Z.(- one))) (parse_num e)
     | { Expr.term = Expr.App ({ Expr.builtin = A.Op A.Sum}, [], l) } ->
-      CCOpt.((sequence_l (List.map parse_num l)) >|= List.fold_left add zero)
+      CCOption.((sequence_l (List.map parse_num l)) >|= List.fold_left add zero)
     | { Expr.term = Expr.App ({ Expr.builtin = A.Op A.Difference}, [], [a; b]) } ->
-      CCOpt.map2 diff (parse_num a) (parse_num b)
+      CCOption.map2 diff (parse_num a) (parse_num b)
     | { Expr.term = Expr.App (
         { Expr.builtin =  (A.Op A.Product)}, [],
         ([ { Expr.term = Expr.App ({ Expr.builtin = A.Val v}, [], []) }; e] |
          [ e; { Expr.term = Expr.App ({ Expr.builtin = A.Val v}, [], []) }] ) ) } ->
-      CCOpt.map (times v) (parse_num e)
+      CCOption.map (times v) (parse_num e)
     | { Expr.t_type = { Expr.ty = Expr.TyApp ({ Expr.builtin = A.Type _ }, []) } } as e ->
       Some (monome Q.one e)
     | _ -> None
diff --git a/static/Makefile b/static/Makefile
index 4329632..d7a8c11 100644
--- a/static/Makefile
+++ b/static/Makefile
@@ -18,8 +18,8 @@ clean:
 # ========
 
 DK_FILES=logic.dko classical.dko epsilon.dko
-DKC  := $(shell command -v dkcheck 2> /dev/null)
-DKD  := $(shell command -v dkdep 2> /dev/null)
+DKC  := $(shell command -v dk 2> /dev/null) check
+DKD  := $(shell command -v dk 2> /dev/null) dep
 
 dk: $(DK_FILES)
 
@@ -35,7 +35,7 @@ include .depend
 
 .depend:
 ifdef DKD
-	dkdep -o .depend *.dk
+	$(DKD) -o .depend *.dk
 else
 	echo "Skipping dependency analysis"
 endif
@@ -47,7 +47,7 @@ endif
 
 %.dko: %.dk
 ifdef DKC
-	dkcheck -e $<
+	$(DKC) -e $<
 else
 	echo "Skipping compilation of $<"
 endif