diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3a1f785e73ea8494df86a983af9ee7dd1c47e460..5bcbea0e23eccf3db34a85d6453e8e4544decf00 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -96,9 +96,9 @@ let rec expr_to_coq (r : expr) : Formula.t =
                           | Div   -> Infix(expr_to_coq x,"/",expr_to_coq y) 
                           | And   -> Infix(expr_to_coq x,"&&",expr_to_coq y) 
                           | Or    -> Infix(expr_to_coq x,"||",expr_to_coq y) 
-                          | Sup   -> Infix(expr_to_coq x,">",expr_to_coq y) 
-                          | Inf   -> Infix(expr_to_coq x,"<",expr_to_coq y) 
-                          | Equal -> Infix(expr_to_coq x,"==",expr_to_coq y) 
+                          | Sup   -> App(Cst "gt",[expr_to_coq x;expr_to_coq y]) 
+                          | Inf   -> App(Cst "lt",[expr_to_coq x;expr_to_coq y]) 
+                          | Equal -> App(Cst "eq",[expr_to_coq x;expr_to_coq y]) 
                           | Diff  -> Infix(expr_to_coq x,"!=",expr_to_coq y) 
                           )
       | Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))