From 5dcd9ee54d0dba9e0ae1064d37be1a379d8d9ec9 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Tue, 16 Jul 2024 12:17:21 +0200
Subject: [PATCH] typo
---
lib/gencoq.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3c2a4b1..4cbe2ec 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
--
GitLab