.

src/lib/EAFormula.ml

@@ -14,7 +14,7 @@ type eaformula =
   | EX of string * eaformula (* exists, diamond of K *)
   | AX of string * eaformula (* forall, box of K *)
   | ID of eaformula (* modality of the identity functor *)
-  | E of eaformula (* global diamond *)
+  | E_AP of string (* global diamond *)
   | A of eaformula (* global box *)
 
 let rec exportFormula_buffer sb f =
@@ -67,9 +67,8 @@ let rec exportFormula_buffer sb f =
   | ID f1 ->
       Buffer.add_string sb "0";
       prio 4 f1
-  | E f1 ->
-      Buffer.add_string sb "E ";
-      prio 4 f1
+  | E_AP s ->
+      Buffer.add_string sb "E "
   | A f1 ->
       Buffer.add_string sb "A ";
       prio 4 f1
@@ -82,7 +81,7 @@ let exportFormula f =
 let rec nom2EA f = match f with
   | CoAlgFormula.FALSE -> FALSE
   | CoAlgFormula.AP a -> AP a
-  | CoAlgFormula.AND (a, b) -> E (AND (nom2EA a, nom2EA b))
+  | CoAlgFormula.AND (a, b) -> A (AND (nom2EA a, nom2EA b))
   | _ -> TRUE
         
 (* vim: set et sw=2 sts=2 ts=8 : *)

src/lib/EAFormula.mli

@@ -14,7 +14,7 @@ type eaformula =
   | EX of string * eaformula (* exists, diamond of K *)
   | AX of string * eaformula (* forall, box of K *)
   | ID of eaformula (* modality of the identity functor *)
-  | E of eaformula (* global diamond *)
+  | E_AP of string (* global diamond *)
   | A of eaformula (* global box *)
 
 val exportFormula : eaformula -> string