From c318b21541f8d95ce5611d9ca17c4f4cdb5e3f18 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 16 May 2024 11:04:03 +0200
Subject: [PATCH] [wp] Fixed typo
---
src/plugins/wp/Why3Import.ml | 12 ++++--------
1 file changed, 4 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 812824cd340..75b1dd56dcd 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -59,9 +59,8 @@ let of_infix s =
let construct_acsl_name (id : W.Ident.ident) =
let (paths,name,scopes) = T.restore_path id in
match List.rev scopes with
- | (t::q) ->
- let modscopes = List.rev_append q [(of_infix t)] in
- String.concat "::" (paths @ name::modscopes)
+ | (t::q) ->
+ String.concat "::" (paths @ name :: List.rev_append q [of_infix t])
| [] -> ""
@@ -128,10 +127,7 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
List.fold_right
(fun (tv: W.Ty.tvsymbol) (txs,tvs) ->
let x = tv.tv_name.id_string in
- match x with
- | "int" -> x :: txs, W.Ty.Mtv.add tv (C.Linteger) tvs
- | "real" -> x :: txs, W.Ty.Mtv.add tv (C.Lreal) tvs
- | _ -> x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
+ x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
) txs ([], W.Ty.Mtv.empty)
@@ -230,7 +226,7 @@ let import_theory env (tenv:tenv) (lenv:lenv) thname =
let li = li_of_ls tenv ls lenv in
L.debug ~level:2 "Corresponding dlogic LTI %a" pp_li li;
) dlogics
- | _ -> L.debug ~level:2 "Decl but whatever"
+ | _ -> L.debug ~level:2 "Decl and whatever"
end
| Use _| Clone _| Meta _ -> L.debug ~level:2 ""
) theory.th_decls
--
GitLab