Doc std_types cont.

Author: svorenova

src/util/std_types.h

@@ -946,6 +946,8 @@ inline code_typet &to_code_type(typet &type)
 }
 
 /// Arrays with given size
+///
+/// Used for ordinary source-language arrays.
 class array_typet:public type_with_subtypet
 {
 public:
@@ -1525,7 +1527,14 @@ inline const range_typet &to_range_type(const typet &type)
   return static_cast<const range_typet &>(type);
 }
 
-/// The C vector type
+/// The vector type
+///
+/// Used to represent the short vectors used by CPU instruction sets such as
+/// MMX, SSE and AVX. They all provide registers that are something like
+/// 8 x int32, for example, and corresponding operations that operate
+/// element-wise on their operand vectors. Compared to \ref array_typet
+/// that has no element-wise operators. Note that `remove_vector.h` removes
+/// this data type by compilation into arrays.
 class vector_typet:public type_with_subtypet
 {
 public: