diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index bd52c9dc7bda66cd4a7d37e6c6e474fe04db7095..14e2806343234c1e3359e5cac5703ec6e5a276a8 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -118,6 +118,10 @@ let rec sizeFormula f =
   | MU (_, f1)
   | NU (_, f1) -> succ (succ (sizeFormula f1))
   | VAR _ -> 1
+  | AF _ | EF _
+  | AG _ | EG _
+  | AU _ | EU _ ->
+			raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
 
 (** Determines the size of a sorted formula.
     @param f A sorted formula.
@@ -509,7 +513,16 @@ let rec exportTatlFormula_buffer sb f =
   | ID _
   | NORM _
   | NORMN _
-  | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+  | FUS _
+  | MU _
+  | NU _
+  | VAR _
+  | AF _
+  | EF _
+  | AG _
+  | EG _
+  | AU _
+  | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
 
 let exportTatlFormula f =
   let sb = Buffer.create 128 in
@@ -983,6 +996,12 @@ let rec nnfNeg f =
   | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
   | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)  
   | FUS (first, f1) -> FUS (first, nnfNeg f1)
+  | AF _
+  | EF _
+  | AG _
+  | EG _
+  | AU _
+  | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
       
 (** Converts a formula to negation normal form
     by "pushing in" the negations "~".
@@ -1064,6 +1083,12 @@ and nnf f =
       let ft = nnf f1 in
       if ft == f1 then f else FUS (first, ft)
 
+  | AF _
+  | EF _
+  | AG _
+  | EG _
+  | AU _
+  | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
 
 (** Simplifies a formula.
     @param f A formula which must be in negation normal form.
@@ -1235,6 +1260,13 @@ let rec simplify f =
         | _ -> if ft == f1 then f else FUS (first, ft)
       end
 
+  | AF _
+  | EF _
+  | AG _
+  | EG _
+  | AU _
+  | EU _ ->
+	 raise (CoAlgException ("nnf: CTL should have been removed at this point"))
 
 (** Destructs an atomic proposition.
     @param f An atomic proposition.
@@ -1914,7 +1946,13 @@ let rec hc_formula hcF f =
   | FUS (first, f1) ->
       let tf1 = hc_formula hcF f1 in
       HcFormula.hashcons hcF (HCFUS (first, tf1))
-
+  | AF _
+  | EF _
+  | AG _
+  | EG _
+  | AU _
+  | EU _ ->
+	 raise (CoAlgException ("nnf: CTL should have been removed at this point"))
 
 (** An instantiation of a hash table (of the standard library)
     for hash-consed formulae. The test for equality