typo

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