From 004eebeea19bd9c35de76caee41cfa0ec431f9ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 10:11:48 +0000
Subject: [PATCH] [modules] formatting
---
src/kernel_services/ast_queries/logic_typing.ml | 17 ++++++++---------
1 file changed, 8 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 99e31d81f6..2b115f6ab6 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -752,8 +752,13 @@ struct
let add_import ?(current=false) ?alias name =
begin
- let short = match alias with Some "_" -> "" | Some a -> a | None ->
- List.hd @@ List.rev @@ Logic_utils.longident name in
+ let short =
+ match alias with
+ | Some "_" -> ""
+ | Some a -> a
+ | None ->
+ List.hd @@ List.rev @@ Logic_utils.longident name
+ in
let s = {
long_prefix = name ^ "::";
short_prefix = short ^ "::";
@@ -2812,8 +2817,7 @@ struct
in make_expr f
with Not_found ->
ctxt.error loc
- "invalid use of overloaded function \
- %s as constant" x
+ "invalid use of overloaded function %s as constant" x
end
| PLapp (f, labels, tl) ->
let env = drop_qualifiers env in
@@ -3390,7 +3394,6 @@ struct
tt
and type_bool_term ctxt env t =
- let module [@warning "-60"] C0 = struct end in
let tt = ctxt.type_term ctxt env t in
if not (plain_boolean_type tt.term_type) then
ctxt.error t.lexpr_loc "boolean expected but %a found"
@@ -3398,7 +3401,6 @@ struct
mk_cast tt (Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[]))
and type_num_term_option ctxt env t =
- let module [@warning "-60"] C = struct end in
match t with
None -> None, Linteger (* Warning: should be an hybrid of integer
and float. *)
@@ -3454,7 +3456,6 @@ struct
| _ -> [], ctxt.type_predicate ctxt env p0
let term_lval_assignable ctxt ~accept_formal ~accept_const env t =
- let module [@warning "-60"] C = struct end in
let t = ctxt.type_term ctxt env t in
let mode = { lval_assignable_mode with accept_formal ; accept_const } in
if not (check_lval_kind mode t) then
@@ -3463,7 +3464,6 @@ struct
lift_set (term_lval (fun _ t -> t)) t
let term ctxt env t =
- let module [@warning "-60"] C = struct end in
match t.lexpr_node with
| PLnamed(name,t) ->
let t = ctxt.type_term ctxt env t in
@@ -3473,7 +3473,6 @@ struct
{ term_node = t'; term_loc=t.lexpr_loc; term_type=ty; term_name = [] }
let predicate ctxt env p0 =
- let module [@warning "-60"] C = struct end in
let loc = p0.lexpr_loc in
let predicate = ctxt.type_predicate ctxt in
let term = ctxt.type_term ctxt in
--
GitLab