Skip to content
Snippets Groups Projects
Commit 1c16e62e authored by Kylian Fontaine's avatar Kylian Fontaine
Browse files

Merge branch 'main' into 'module' 

# Conflicts:
#   lib/gencoq.ml
parents 2b843ee7 5dcd9ee5
No related branches found
No related tags found
1 merge request!1Module
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 3 deletions
lib/gencoq.ml
+ 3
− 3
View file @ 1c16e62e
......@@ -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]))
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment