diff --git a/marzipan/TODO.md b/marzipan/TODO.md
index 88c82eb..2cd2db9 100644
--- a/marzipan/TODO.md
+++ b/marzipan/TODO.md
@@ -33,11 +33,12 @@
 * ~~exception handling in analyze() and in run_proverif()~~
 * ~~refactor filtering in run_proverif (see karo's comment)~~
 * ~configurable target directory~
+* ~lark parser: multiline comments, how???~
 
 ## Next Steps
 
 * integrate marzipan.awk into Python, somehow
-  * lark parser: multiline comments, how???
+  * options term special cases (c.f. manual page 133, starting with "fun" term)
 * rewrite marzipan.awk into Python/LARK
   * define a LARK grammar for marzipan.awk rules
   * write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv)
@@ -54,6 +55,6 @@
     * and rewrite the AST within Python
     * reconstruct ProVerif input file for ProVerif
   * rewrite our CPP usages into Python/…?
-
+* low priority: nested comments in ProVerif code
 
 “it replaces the Bash script and is idiomatic Python code”
diff --git a/marzipan/src/parser.py b/marzipan/src/parser.py
index 98068ee..9e9dedc 100644
--- a/marzipan/src/parser.py
+++ b/marzipan/src/parser.py
@@ -33,7 +33,13 @@ proverif_grammar = Lark(
     _non_empty_seq{x}: x ("," x)*
     _maybe_empty_seq{x}: [ _non_empty_seq{x} ]
 
+    IDENT_FUN_CONST: "data" | "private" | "typeConverter"
+    IDENT_FREE_REDUC: "private"
+    IDENT_PRED: "memberOptim" | "block"
+    IDENT_PROCESS: "precise"
+    IDENT_QUERY_LEMMA_AXIOM: "noneSat" | "discardSat" | "instantiateSat" | "fullSat" | "noneVerif" | "discardVerif" | "instantiateVerif" | "fullVerif"
     options: [ "[" _non_empty_seq{IDENT} "]" ]
+    options{idents}: [ "[" _non_empty_seq{idents} "]" ]
     process: ZERO
            | YIELD
            | IDENT [ "(" _maybe_empty_seq{pterm} ")" ]
@@ -193,6 +199,7 @@ proverif_grammar = Lark(
         | nounif_decl
         | elimtrue_decl
         | clauses_decl
+        | module_decl
         #| param_decl
         #| proba_decl
         #| letproba_decl
@@ -204,7 +211,7 @@ proverif_grammar = Lark(
     channel_decl: "channel" _non_empty_seq{IDENT} "."
     free_decl: "free" _non_empty_seq{IDENT} ":" typeid options "."
     const_decl: "const" _non_empty_seq{IDENT} ":" typeid options "."
-    fun_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid options "."
+    fun_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid options{IDENT_FUN_CONST} "."
     letfun_decl: "letfun" IDENT [ "(" [ typedecl ] ")" ] "=" pterm "."
     reduc_decl: "reduc" eqlist options "."
     fun_reduc_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid "reduc" mayfailreduc options "."
@@ -328,6 +335,8 @@ proverif_grammar = Lark(
     elimtrue_decl: "elimtrue" [ failtypedecl ";" ] term "."
     clauses_decl: "clauses" clauses "."
 
+    module_decl: "@module" " " IDENT
+
     # TODO: finish defining these (comes from Cryptoverif)
     #param_decl: "param" _non_empty_seq{IDENT} options "."
     #proba_decl: "proba" IDENT ["(...)"] options "."