From 380bfa802d3f2a16d2b594a1430bfbe44b9a6396 Mon Sep 17 00:00:00 2001 From: Klaas Pruiksma Date: Tue, 23 Dec 2025 13:13:25 +0100 Subject: [PATCH] Adds support for passing attributes on splices through to the generated parser/serializer, and adds tac_opaque to opaque parsers. --- src/Comparse.Tactic.GenerateParser.fst | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Comparse.Tactic.GenerateParser.fst b/src/Comparse.Tactic.GenerateParser.fst index 710dd0a..dc60650 100644 --- a/src/Comparse.Tactic.GenerateParser.fst +++ b/src/Comparse.Tactic.GenerateParser.fst @@ -857,10 +857,11 @@ let gen_parser_aux type_fv force_smt = lb_def = parser_fun; } in let sv = pack_sigelt (Sg_Let { isrec = false; lbs = [parser_letbinding];}) in - let sv = - if is_opaque then set_sigelt_attrs [(`"opaque_to_smt")] sv - else sv + let attrs = splice_attrs () in + let attrs = + if is_opaque then attrs @ [(`"opaque_to_smt"); (`tac_opaque)] else attrs in + let sv = set_sigelt_attrs attrs sv in [sv] val gen_parser: term -> Tac decls