diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 8b6863586b6519db29415bd9f963a6d66d2f9157..422a926cc9a5ce6958553ed25225c1f1715b6a68 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1644,6 +1644,9 @@ let const_fusion first f1 = FUS (first, f1)
 
 (** Hash-consed formulae, which are in negation normal form,
     such that structural and physical equality coincide.
+
+    Also CTL has been replaced by the equivalent μ-Calculus
+    constructs
  *)
 type hcFormula = (hcFormula_node, formula) HC.hash_consed
 and hcFormula_node =
@@ -1669,6 +1672,9 @@ and hcFormula_node =
   | HCNORMN of hcFormula * hcFormula
   | HCCHC of hcFormula * hcFormula
   | HCFUS of bool * hcFormula
+  | HCMU of string * hcFormula
+  | HCNU of string * hcFormula
+  | HCVAR of string
 
 (** Determines whether two formula nodes are structurally equal.
     @param f1 The first formula node.
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3397ba44a4e8e3ad73e0e00a75786a3eb50037d3..c807b4ec96c332a85e19f9f0ae578307ee3b2e7b 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -155,6 +155,9 @@ and hcFormula_node =
   | HCNORMN of hcFormula * hcFormula
   | HCCHC of hcFormula * hcFormula
   | HCFUS of bool * hcFormula
+  | HCMU of string * hcFormula
+  | HCNU of string * hcFormula
+  | HCVAR of string
 
 module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)