diff --git a/src/core/expr_intf.ml b/src/core/expr_intf.ml
index 4760302f..685e46ff 100644
--- a/src/core/expr_intf.ml
+++ b/src/core/expr_intf.ml
@@ -4,6 +4,10 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+type negated = Formula_intf.negated =
+  | Negated (* changed sign *)
+  | Same_sign (* kept sign *)
+
 module type S = sig
   (** Signature of formulas that parametrises the Mcsat Solver Module. *)
 
@@ -37,7 +41,7 @@ module type S = sig
   val neg : Formula.t -> Formula.t
   (** Formula negation *)
 
-  val norm : Formula.t -> Formula.t * Formula_intf.negated
+  val norm : Formula.t -> Formula.t * negated
   (** Returns a 'normalized' form of the formula, possibly negated
       (in which case return [Negated]).
       [norm] must be so that [a] and [neg a] normalise to the same formula,
diff --git a/src/example/expr.ml b/src/example/expr.ml
index b27264e0..72eef2e1 100644
--- a/src/example/expr.ml
+++ b/src/example/expr.ml
@@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module FI = Formula_intf
+module I = Formula_intf
 
 exception Invalid_var
 
@@ -40,9 +40,9 @@ let neg = function
   | Distinct (a, b) -> Equal (a, b)
 
 let norm = function
-  | Prop i -> Prop (abs i), if i < 0 then FI.Negated else FI.Same_sign
-  | Equal (a, b) -> Equal (a, b), FI.Same_sign
-  | Distinct (a, b) -> Equal (a, b), FI.Negated
+  | Prop i -> Prop (abs i), if i < 0 then I.Negated else I.Same_sign
+  | Equal (a, b) -> Equal (a, b), I.Same_sign
+  | Distinct (a, b) -> Equal (a, b), I.Negated
 
 (* Only used after normalisation, so usual functions should work *)
 let hash = Hashtbl.hash