summaryrefslogtreecommitdiff
path: root/src/parse_ast.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/parse_ast.ml')
-rw-r--r--src/parse_ast.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 362333f3..5eb8038a 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -507,6 +507,7 @@ def = (* Top-level definition *)
| DEF_default of default_typing_spec (* default kind and type assumptions *)
| DEF_scattered of scattered_def (* scattered definition *)
| DEF_reg_dec of dec_spec (* register declaration *)
+ | DEF_pragma of string * string * l
| DEF_internal_mutrec of fundef list