diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index cb2e340d28322eea9c1c485d5e87c52426a8a181..950f7ba02de67f01b472413ed34a00c5f4735d16 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -1,9 +1,9 @@
 /// Dependent types
 
 /// PVS allows dependent types using theory abstraction. For instance,
-/// vector[t: TYPE, n: nat]: THEORY BEGIN vec: TYPE END vector
+/// vector_real[n: nat]: THEORY BEGIN vec: TYPE END vector
 /// allows to define
-/// cons(n: nat, e: t, v: vector[t, n].vec): vector[t, n + 1].vec
+/// cons(n: nat, r: real, v: vector_real[n].vec): vector_real[n + 1].vec
 
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert