From abefdfa97861706ae8f5007a2b10b3a4ee125c75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 12:44:57 +0200
Subject: [PATCH] [modules] useless open/close api
---
src/kernel_services/ast_queries/logic_typing.ml | 13 +------------
src/kernel_services/ast_queries/logic_typing.mli | 6 ------
2 files changed, 1 insertion(+), 18 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ea02461aaf..3328f6fde9 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -658,12 +658,6 @@ sig
val conditional_conversion:
Cil_types.location -> Logic_ptree.relation option ->
Cil_types.term -> Cil_types.term -> Cil_types.logic_type
-
- val add_import : ?current:bool -> ?alias:string -> string -> unit
- val clear_imports : unit -> unit
- val push_imports : unit -> unit
- val pop_imports : unit -> unit
-
val term : Lenv.t -> Logic_ptree.lexpr -> term
val predicate : Lenv.t -> Logic_ptree.lexpr -> predicate
val code_annot :
@@ -735,14 +729,9 @@ struct
| None -> !imported_scopes
| Some s -> s :: !imported_scopes
- let clear_imports () =
- begin
- Stack.clear scopes ;
- current_scope := None ;
- imported_scopes := [] ;
- end
let push_imports () =
Stack.push (!current_scope,!imported_scopes) scopes
+
let pop_imports () =
begin
let c,s = Stack.pop scopes in
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 9af8714ecb..83ed8d4baa 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -181,12 +181,6 @@ sig
Cil_types.location -> Logic_ptree.relation option ->
Cil_types.term -> Cil_types.term -> Cil_types.logic_type
- (** Open module in local environment. *)
- val add_import : ?current:bool -> ?alias:string -> string -> unit
- val clear_imports : unit -> unit
- val push_imports : unit -> unit
- val pop_imports : unit -> unit
-
(** type-checks a term. *)
val term : Lenv.t -> Logic_ptree.lexpr -> term
--
GitLab