diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
index 7708cd9f0c..940248d698 100644
--- a/src/Assembly/Parse.v
+++ b/src/Assembly/Parse.v
@@ -588,6 +588,7 @@ Fixpoint get_initial_data (ls : Lines) : list (AccessSize * list Z)
           | LABEL _
           | EMPTY
           | GLOBAL _
+          | DIRECTIVE _
           | DEFAULT_REL
             => get_initial_data ls
           | SECTION _