diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3c2a4b11b5ef97570df064cca815aba5641b958c..4cbe2ecbb9a55dedf49635267b6a15c3e3e31f6b 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) 
                           | Impli  -> Infix(expr_to_coq x, "->", expr_to_coq y) 
                           | Equiv  -> Infix(expr_to_coq x,"<->",expr_to_coq y) 
@@ -441,6 +441,7 @@ let generate_lt =
     moving robogram da config <> nil ->
     lt_config (round robogram da config) config."]) ::[]
 
+
 (**[generate_coq d s] generated from the complete description (world, robogram, measure) [d] the named coq instance [s]
     @param description of
     @param string s