diff --git a/src/cc/expl.mli b/src/cc/expl.mli
index 24618076..efa26063 100644
--- a/src/cc/expl.mli
+++ b/src/cc/expl.mli
@@ -28,20 +28,20 @@ val mk_congruence : E_node.t -> E_node.t -> t
 val mk_theory :
   Term.t -> Term.t -> (Term.t * Term.t * t list) list -> Proof_term.step_id -> t
 (** [mk_theory t u expl_sets pr] builds a theory explanation for
-        why [|- t=u]. It depends on sub-explanations [expl_sets] which
-        are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
-        explanations that justify [t_i = u_i] in the current congruence closure.
+    why [|- t=u]. It depends on sub-explanations [expl_sets] which
+    are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
+    explanations that justify [t_i = u_i] in the current congruence closure.
 
-        The proof [pr] is the theory lemma, of the form
-        [ (t_i = u_i)_i |- t=u ].
-        It is resolved against each [expls_i |- t_i=u_i] obtained from
-        [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
-        where [Gamma] is a subset of the literals asserted into the congruence
-        closure.
+    The proof [pr] is the theory lemma, of the form
+    [ (t_i = u_i)_i |- t=u ].
+    It is resolved against each [expls_i |- t_i=u_i] obtained from
+    [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
+    where [Gamma] is a subset of the literals asserted into the congruence
+    closure.
 
-        For example for the lemma [a=b] deduced by injectivity
-        from [Some a=Some b] in the theory of datatypes,
-        the arguments would be
-        [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
-        where [pr] is the injectivity lemma [Some a=Some b |- a=b].
-    *)
+    For example for the lemma [a=b] deduced by injectivity
+    from [Some a=Some b] in the theory of datatypes,
+    the arguments would be
+    [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
+    where [pr] is the injectivity lemma [Some a=Some b |- a=b].
+*)