diff --git a/src/plugins/wp/share/coqwp/Vlist.v b/src/plugins/wp/share/coqwp/Vlist.v
index e758e478dbf012c9840892f530db9a98831f5a4a..e4f1f454f3701d5971d3a63f8dde040dc91548da 100644
--- a/src/plugins/wp/share/coqwp/Vlist.v
+++ b/src/plugins/wp/share/coqwp/Vlist.v
@@ -60,7 +60,7 @@ Defined.
 
 (* Why3 goal *)
 Definition concat {a:Type} {a_WT:WhyType a} : (list a) -> (list a) -> list a.
-  Open Local Scope list_scope.
+  Local Open Scope list_scope.
   exact(fun u v => u ++ v).
 Defined.