diff --git a/CHANGES.md b/CHANGES.md
index 234467cb0b4eb83edf3d8d2b0032f6483e2fc881..e32fbb4505d133eec166bdb7bde6b59a39189b15 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -16,7 +16,7 @@ Language
     to give the name `Foo` to the corresponding hypothesis after introduction
   * identifiers used for specification (resp. definition) of a function `foo`
     have been renamed from `foo_spec` (resp. `foo_def`) to `foo'spec` (resp. `foo'def`) :x:
-  * identifiers used for goals `VC foo` have been renamed to `foo'VC`
+  * identifiers used for goals `VC foo` have been renamed to `foo'vc`
   * identifiers used for record constructor `mk foo` have been renamed to `foo'mk` :x:
   * the `alias` clause can now be used in program functions to force the aliasing
     of function parameters and/or named returns
diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml
index 9129a250dd7081d80c22674d8ad9199f5422fb90..955e601a25779e0083a2e2916f170ec10fa3d0ef 100644
--- a/src/mlw/pmodule.ml
+++ b/src/mlw/pmodule.ml
@@ -1048,7 +1048,7 @@ let clone_type_decl inst cl tdl kn =
 let add_vc uc (its, f) =
   let {id_string = nm; id_loc = loc} = its.its_ts.ts_name in
   let attrs = Sattr.singleton (Ident.create_attribute ("expl:VC for " ^ nm)) in
-  let pr = create_prsymbol (id_fresh ~attrs ?loc (nm ^ "'VC")) in
+  let pr = create_prsymbol (id_fresh ~attrs ?loc (nm ^ "'vc")) in
   let d = create_pure_decl (create_prop_decl Pgoal pr f) in
   add_pdecl ~warn:false ~vc:false uc d
 
diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml
index edfd10c89794aa8354ff0f7de3226133bde885ed..5c30b2e973e724e712e32cd1b68df2b57e87b390 100644
--- a/src/mlw/vc.ml
+++ b/src/mlw/vc.ml
@@ -1547,7 +1547,7 @@ let mk_vc_decl ({known_map = kn} as env) id f =
   let {id_string = nm; id_attrs = attrs; id_loc = loc} = id in
   let attrs = if attrs_has_expl attrs then attrs else
     Sattr.add (Ident.create_attribute ("expl:VC for " ^ nm)) attrs in
-  let pr = create_prsymbol (id_fresh ~attrs ?loc (nm ^ "'VC")) in
+  let pr = create_prsymbol (id_fresh ~attrs ?loc (nm ^ "'vc")) in
   let f = wp_forall (Mvs.keys (t_freevars Mvs.empty f)) f in
   let f = Typeinv.inject kn f in
   let f = if Debug.test_flag debug_no_eval then f else