From ceed3abaeb7c6de314454d9d4c12aeb93dbecbb6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 19 Dec 2019 13:38:23 +0100
Subject: [PATCH] [wp] fixes typo in error message
---
src/plugins/wp/ProverWhy3.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 61f6651c442..488d62b73e3 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -741,7 +741,7 @@ class visitor (ctx:context) c =
| [ th ] -> self#add_import th
| [ th ; was ] -> self#add_import ~was th
| _ -> why3_failure
- "[driver] incorrect why3.file %S for library '%s'"
+ "[driver] incorrect why3.import %S for library '%s'"
opt thy
) (Str.split regexp_com opt)
in
--
GitLab