diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml index 605dfc94936942a82a789ce4e99930e0a3a0d8c1..563650cc96283a5924a6dc6291b81ad54f37339e 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