From 9aa687fe0abbbd38723fb64910551d2900048915 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 8 Jul 2024 15:57:17 +0200
Subject: [PATCH] [wp] Removed error throwing
---
src/plugins/wp/Why3Import.ml | 2 --
1 file changed, 2 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 605dfc94936..563650cc962 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -309,8 +309,6 @@ let import_theory (env : env) thname =
types = List.rev menv.lti;
paths = theory_path };
end
- else
- L.error "Trying to register %s a second time, ignoring" thname;
with W.Env.LibraryNotFound _ ->
L.error "Library %s not found" thname
--
GitLab