Commit 24bc00a831f74cd95255f94660d4763db4b6761e

Philipp Wiesemann 2016-08-03T22:39:44

Fixed two old identifiers in header comments.